Sun, 22 Apr 2012 15:51:03 -0400 |
Adam Chlipala |
Citations for continuations and unification |
Sun, 22 Apr 2012 15:38:11 -0400 |
Adam Chlipala |
Define 'certified program' |
Fri, 20 Apr 2012 12:49:47 -0400 |
Adam Chlipala |
Typo fixes |
Thu, 12 Apr 2012 18:46:55 -0400 |
Adam Chlipala |
Typo fix |
Thu, 12 Apr 2012 18:45:48 -0400 |
Adam Chlipala |
New release |
Thu, 12 Apr 2012 18:41:32 -0400 |
Adam Chlipala |
Comment CpdtTactics.v |
Thu, 12 Apr 2012 16:27:28 -0400 |
Adam Chlipala |
Baffling unification messages explained |
Thu, 12 Apr 2012 15:54:37 -0400 |
Adam Chlipala |
A pass over Large |
Thu, 12 Apr 2012 14:30:53 -0400 |
Adam Chlipala |
A pass through Match |
Thu, 12 Apr 2012 12:11:29 -0400 |
Adam Chlipala |
More discussion of axiom avoidance and tactic pitfalls for JMeq |
Sun, 08 Apr 2012 11:11:27 -0400 |
Adam Chlipala |
Strengthen last theorem of Coinductive |
Tue, 03 Apr 2012 15:10:04 -0400 |
Adam Chlipala |
Conclusion |
Sun, 01 Apr 2012 15:14:44 -0400 |
Adam Chlipala |
Typo fixes |
Sun, 01 Apr 2012 15:02:32 -0400 |
Adam Chlipala |
New chapter: ProgLang |
Thu, 29 Mar 2012 18:10:52 -0400 |
Adam Chlipala |
Get it to build with Coq 8.4 |
Thu, 29 Mar 2012 17:15:14 -0400 |
Adam Chlipala |
Date increment |
Thu, 29 Mar 2012 17:13:23 -0400 |
Adam Chlipala |
Recursing under binders in reification |
Wed, 28 Mar 2012 13:20:50 -0400 |
Adam Chlipala |
One more example of avoiding axioms (getNat) |
Mon, 26 Mar 2012 17:00:34 -0400 |
Adam Chlipala |
New release |
Mon, 26 Mar 2012 16:55:59 -0400 |
Adam Chlipala |
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default |
Mon, 26 Mar 2012 16:24:19 -0400 |
Adam Chlipala |
Prose for third LogicProg section |
Mon, 26 Mar 2012 16:04:52 -0400 |
Adam Chlipala |
Prose for second LogicProg section |
Mon, 26 Mar 2012 15:35:09 -0400 |
Adam Chlipala |
Prose for first LogicProg section |
Fri, 02 Mar 2012 10:52:22 -0500 |
Adam Chlipala |
The one rule of dependent pattern matching |