User loginNavigation 
Certified Programming With Dependent Types Goes BetaCertified Programming With Dependent Types From the introduction:
This is the best Coq tutorial that I know of, partially for being comprehensive, and partially for taking a very different tack than most with Adam's emphasis on proof automation using Coq's Ltac tactic language. It provides an invaluable education toward understanding what's going on either in LambdaTamer or Ynot, both of which are important projects in their own rights. Please note that Adam is explicitly requesting feedback on this work. By Paul Snively at 20100109 16:56  Functional  Lambda Calculus  Logic/Declarative  Misc Books  Semantics  Teaching & Learning  Type Theory  other blogs  10873 reads

Browse archives
Active forum topics 
Recent comments
16 weeks 4 days ago
16 weeks 4 days ago
16 weeks 4 days ago
38 weeks 5 days ago
43 weeks 8 hours ago
44 weeks 4 days ago
44 weeks 4 days ago
47 weeks 2 days ago
51 weeks 6 days ago
51 weeks 6 days ago