Formal Proof

i have set up this page to help organize resources and information related to our reading course on proof assistants.

online resources

web sites

• ProofWeb lets you use Coq through your web browser
• Twelf Live does the same for Twelf

articles

• the December 2008 issue of the AMS Notices has a few articles on formal proof
• Herman Geuvers just wrote a nice survey of formal proof with proof assistants
• Robert Harper has a good paper on LF as foundation for Twelf

books

• Adam Chlipala is writing a book about Certified Programming with Dependent Types using Coq
• Robert Harper is writing a book about Practical Foundations for Programming Languages