3 ms·

Are there any good resources (similarly short and informal) about doing proofs in Coq? I don't have anything particular to prove, but I find it interesting and

by paulgb 7y ago

Are there any good resources (similarly short and informal) about doing proofs in Coq? I don't have anything particular to prove, but I find it interesting and would like to build up intuition for the Curry-Howard Correspondence. Also, more tangential, but this comment section might attract people who know the answer: any good resources for getting started on type systems more generally?

lexpar 7y ago
I took a graduate class where we worked though the first and second volumes of Software Foundations (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/). These are very nice introductions to the Coq environment and are being actively improved. The textbook is available online, with the source file of each chapter being a valid coq script, making it easy to experiment. There are also a large amount of interesting and challenging exercises. Here's a link to the chapter on the Curry-Howard correspondence: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...
kryptiskt 7y ago
Software Foundations (https://softwarefoundations.cis.upenn.edu https://softwarefoundations.cis.upenn.edu) is pretty informal and understandable, what it isn't is short. But it's a very useful resource. The best general introduction is probably still Types and Programming Languages: (https://www.cis.upenn.edu/~bcpierce/tapl/index.html https://www.cis.upenn.edu/~bcpierce/tapl/index.html) It's a great book, but it doesn't get to dependent types.
- ouid 7y ago
  It should be mentioned that software foundations is basically a videogame that you can play in your coq interpreter. Short is less relevant than fun, imo.
- polymatter 7y ago
  I will second that Types and Programming languages is a great book. The next book, https://www.cis.upenn.edu/~bcpierce/attapl/index.html https://www.cis.upenn.edu/~bcpierce/attapl/index.html does get into Dependent Types.
- goodmattg 7y ago
  I'm currently in Prof. Pierce's class at UPenn! Can confirm this is a great book, and we literally work through the exercises. Taking this class AFTER using Scala in industry has really put a lot into context. It's so easy to start too - download CoqIDE or ProofGeneral and get to it!
topmonk 7y ago
If you know Haskell, or are willing to learn, this is a brilliant explanation with code (you build a dependently typed language as you go). It ramps you up very fast yet each step is accessible. This alone really caused me to get bit by the dependent type bug. https://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html?m=1 https://augustss.blogspot.com/2007/10/simpler-easier-in-rece... Here is the example code from this post https://github.com/scott-fleischman/simpler-easier?files=1 https://github.com/scott-fleischman/simpler-easier?files=1
cinnamonheart 7y ago
>Also, more tangential, but this comment section might attract people who know the answer: any good resources for getting started on type systems more generally? I like Philip Wadler's Programming Language Foundations in Agda: https://plfa.github.io/ https://plfa.github.io/ >The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write. I found Agda + PLFA was more approachable for me than Coq + Software Foundations. (Edit: clarifying that I'm responding to the tangent.)
philzook 7y ago
Short and informal is hard to come by here, especially by such a formal system built by such formal people. This tutorial maybe? https://coq.inria.fr/tutorial-nahas https://coq.inria.fr/tutorial-nahas This particular chapter of Software Foundations may be helpful (or it might not be. If so don't sweat it, it isn't really meant to be read in isolation) https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...
ibic 7y ago
I found this one quite useful from the aspect of proving (I'm reading it half way): https://coq.inria.fr/tutorial-nahas https://coq.inria.fr/tutorial-nahas At the end of the article, there is a coq source code of the entire article for you to play with in CoqIDE or Proof General: https://mdnahas.github.io/doc/nahas_tutorial.v https://mdnahas.github.io/doc/nahas_tutorial.v

by paulgb 7y ago

lexpar 7y ago

I took a graduate class where we worked though the first and second volumes of Software Foundations (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/). These are very nice introductions to the Coq environment and are being actively improved. The textbook is available online, with the source file of each chapter being a valid coq script, making it easy to experiment. There are also a large amount of interesting and challenging exercises. Here's a link to the chapter on the Curry-Howard correspondence: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...

kryptiskt 7y ago

Software Foundations (https://softwarefoundations.cis.upenn.edu https://softwarefoundations.cis.upenn.edu) is pretty informal and understandable, what it isn't is short. But it's a very useful resource. The best general introduction is probably still Types and Programming Languages: (https://www.cis.upenn.edu/~bcpierce/tapl/index.html https://www.cis.upenn.edu/~bcpierce/tapl/index.html) It's a great book, but it doesn't get to dependent types.

ouid 7y ago
It should be mentioned that software foundations is basically a videogame that you can play in your coq interpreter. Short is less relevant than fun, imo.
polymatter 7y ago
I will second that Types and Programming languages is a great book. The next book, https://www.cis.upenn.edu/~bcpierce/attapl/index.html https://www.cis.upenn.edu/~bcpierce/attapl/index.html does get into Dependent Types.
goodmattg 7y ago
I'm currently in Prof. Pierce's class at UPenn! Can confirm this is a great book, and we literally work through the exercises. Taking this class AFTER using Scala in industry has really put a lot into context. It's so easy to start too - download CoqIDE or ProofGeneral and get to it!

topmonk 7y ago

If you know Haskell, or are willing to learn, this is a brilliant explanation with code (you build a dependently typed language as you go). It ramps you up very fast yet each step is accessible. This alone really caused me to get bit by the dependent type bug. https://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html?m=1 https://augustss.blogspot.com/2007/10/simpler-easier-in-rece... Here is the example code from this post https://github.com/scott-fleischman/simpler-easier?files=1 https://github.com/scott-fleischman/simpler-easier?files=1

cinnamonheart 7y ago

>Also, more tangential, but this comment section might attract people who know the answer: any good resources for getting started on type systems more generally? I like Philip Wadler's Programming Language Foundations in Agda: https://plfa.github.io/ https://plfa.github.io/ >The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write. I found Agda + PLFA was more approachable for me than Coq + Software Foundations. (Edit: clarifying that I'm responding to the tangent.)

philzook 7y ago

Short and informal is hard to come by here, especially by such a formal system built by such formal people. This tutorial maybe? https://coq.inria.fr/tutorial-nahas https://coq.inria.fr/tutorial-nahas This particular chapter of Software Foundations may be helpful (or it might not be. If so don't sweat it, it isn't really meant to be read in isolation) https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html https://softwarefoundations.cis.upenn.edu/lf-current/ProofOb...

ibic 7y ago

I found this one quite useful from the aspect of proving (I'm reading it half way): https://coq.inria.fr/tutorial-nahas https://coq.inria.fr/tutorial-nahas At the end of the article, there is a coq source code of the entire article for you to play with in CoqIDE or Proof General: https://mdnahas.github.io/doc/nahas_tutorial.v https://mdnahas.github.io/doc/nahas_tutorial.v