rafaeldff + proof   13

The Difference between Recursion & Induction : Inside 206-105
Recursion and induction are closely related. When you were first taught recursion in an introductory computer science class, you were probably told to use induction to prove that your recursive algorithm was correct. Induction suspiciously resembles recursion: the similarity comes from the fact that the inductive hypothesis looks a bit like the result of a “recursive call” to the theorem you are proving. If an ordinary recursive computation returns plain old values, you might wonder if an “induction computation” returns proof terms (which, by the Curry-Howard correspondence, could be thought of as a value).

As it turns out, however, when you look at recursion and induction categorically, they are not equivalent!
recursion  induction  blog  post  EdwardZYang  EdwardYang  math  CT  CategoryTheory  proof  proofs  ProofTheory  Theorem  TheoremProver 
april 2013 by rafaeldff
Certified Programming with Dependent Types
This is the web site for an in-progress textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.
book  online  free  coq  theorem  prooving  program  proof  proofs  ProofAssistant  language  programming 
november 2011 by rafaeldff
Proof Theory and Philosophy (pdf)
"First, propositional logic; second, quantifiers, identity and existence; third, modality and truth. In each part, the first chapter covers logical tools and techniques suited to the topic under examination. The second chapter both discusses the issues th
book  online  GregRestall  free  textbook  logic  philosophy  proof  ProofTheory  theory  modal  propositional  predicate  mathmatics  math  pdf 
december 2006 by rafaeldff
A tutorial on the universality and expressiveness of fold
"This article is a tutorial on two key aspects of the fold operator for lists. [1:] we emphasize the use of the universal property of fold [] as a proof principle [], and as a definition principle[]. [2:], we show that [] the fold operator has greater exp
paper  functional  programming  haskell  fold  function  operator  GrahamHutton  CS  computerscience  proof  formal  formalism  language 
december 2006 by rafaeldff
Formalizing 100 Theorems
Starting from a list of the (admittedly arbitrary) 100 most important theorems in mathematics, the author compiled a list of how many of them have been formalized (w/ theorem provers).
math  mathematics  theorem  theorems  proof  proofs  logic  prover  automatic  theoremproving  list  catalog 
october 2006 by rafaeldff
Practical Foundations of Mathematics
Full-version (html) of a book covering logic, set theory, category theory, etc
PaulTaylor  book  online  mathematics  math  proof  formal  formalism  logic  set  theory  SetTheory  free  systems  system  foundations  category  CategoryTheory  Cambridge. 
june 2006 by rafaeldff
consequently.org/edit: Proof and Counterexample
Wiki about Greg Restall's book on logic with a proof theoretic approach. Has drafts.
logic  book  proof  prooftheory  wiki  GregRestall 
february 2005 by rafaeldff

related tags

4color  4colour  Agda  article  assoc  automatic  blog  book  calculus  Cambridge.  catalog  category  CategoryTheory  Church  computation  computerscience  computing  conjecture  ConorMcBride  coq  cs  CT  Curry-Howard  EdwardYang  EdwardZYang  example  ExistentialType  fold  formal  formalism  foundations  FourColor  FourColour  FP  FrancisJeffryPelletier  FrancisPelletier  free  Frege  function  functional  Functionalprogramming  Gentzen  GrahamHutton  graph  graphs  GraphTheory  GregRestall  haskell  history  induction  lambda  LambdaCalculus  language  list  logic  LtU  math  mathematics  mathmatics  Microsoft  MicrosoftResearch  modal  NaturalDeduction  NewScientist  online  operator  paper  PaulTaylor  pdf  PhilipWadler  philosophy  post  predicate  presentation  program  programming  proof  ProofAssistant  proofs  prooftheory  prooving  propositional  prover  recursion  research  sample  set  SetTheory  system  systems  talk  textbook  theorem  TheoremProver  theoremproving  theorems  theory  type  typing  wiki 

Copy this bookmark: