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 2010-01-09 16:56 | Functional | Lambda Calculus | Logic/Declarative | Misc Books | Semantics | Teaching & Learning | Type Theory | other blogs | 10570 reads
|
Browse archivesActive forum topics |
Recent comments
1 week 2 days ago
5 weeks 3 days ago
6 weeks 18 hours ago
6 weeks 18 hours ago
8 weeks 9 hours ago
8 weeks 9 hours ago
8 weeks 3 days ago
8 weeks 3 days ago
9 weeks 3 days ago
10 weeks 2 days ago