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

Copy this bookmark:

description:

tags: