Fri, 03 Oct 2008 12:44:56 -0400 |
Adam Chlipala |
Code for type-checking example |
Fri, 03 Oct 2008 12:02:44 -0400 |
Adam Chlipala |
sumbool |
Fri, 03 Oct 2008 11:39:59 -0400 |
Adam Chlipala |
Start of Subset |
Wed, 01 Oct 2008 19:53:11 -0400 |
Adam Chlipala |
Publish to Harvard, too |
Wed, 01 Oct 2008 10:07:14 -0400 |
Adam Chlipala |
Template markers for Coinductive |
Wed, 01 Oct 2008 09:56:32 -0400 |
Adam Chlipala |
Finish Coinductive chapter |
Wed, 01 Oct 2008 09:33:44 -0400 |
Adam Chlipala |
Put [try] in front of [subst], to avoid whining about recursive equalities |
Wed, 01 Oct 2008 09:32:36 -0400 |
Adam Chlipala |
Remove [done] markers after enhancement phase finishes |
Tue, 30 Sep 2008 17:47:59 -0400 |
Adam Chlipala |
Co-inductive evaluation example |
Tue, 30 Sep 2008 17:07:57 -0400 |
Adam Chlipala |
Co-equality |
Tue, 30 Sep 2008 16:17:50 -0400 |
Adam Chlipala |
Start of Coinductive |
Tue, 30 Sep 2008 14:02:40 -0400 |
Adam Chlipala |
Make exercises display properly in HTML |
Tue, 30 Sep 2008 13:50:11 -0400 |
Adam Chlipala |
Evaluation exercise |
Tue, 30 Sep 2008 13:11:39 -0400 |
Adam Chlipala |
Beefed-up crush, with auto-inversion and lemma instantiation |
Mon, 29 Sep 2008 14:38:21 -0400 |
Adam Chlipala |
First two exercises |
Sun, 28 Sep 2008 13:52:23 -0400 |
Adam Chlipala |
Update HTML TOC |
Sun, 28 Sep 2008 13:52:06 -0400 |
Adam Chlipala |
Update HTML TOC |
Sun, 28 Sep 2008 13:50:21 -0400 |
Adam Chlipala |
Chapter read-through |
Sun, 28 Sep 2008 13:13:26 -0400 |
Adam Chlipala |
Spell-check |
Sun, 28 Sep 2008 12:44:50 -0400 |
Adam Chlipala |
Merge |
Sun, 28 Sep 2008 12:42:59 -0400 |
Adam Chlipala |
What could go wrong; some exercises |
Sun, 28 Sep 2008 12:44:05 -0400 |
Adam Chlipala |
What could go wrong; some exercises |
Sun, 28 Sep 2008 11:57:15 -0400 |
Adam Chlipala |
Recursive predicates |
Sun, 28 Sep 2008 10:59:04 -0400 |
Adam Chlipala |
Predicates with arguments |
Sat, 27 Sep 2008 16:10:53 -0400 |
Adam Chlipala |
First-order logic |
Sat, 27 Sep 2008 15:31:35 -0400 |
Adam Chlipala |
Constructivity |
Sat, 27 Sep 2008 15:13:01 -0400 |
Adam Chlipala |
[tauto] and [intuition] |
Sat, 27 Sep 2008 14:57:08 -0400 |
Adam Chlipala |
Propositional logic |
Tue, 16 Sep 2008 16:18:11 -0400 |
Adam Chlipala |
Small prose change |
Mon, 15 Sep 2008 10:05:37 -0400 |
Adam Chlipala |
Make Chap. 3 title less grand |
Sat, 13 Sep 2008 14:35:14 -0400 |
Adam Chlipala |
Fix cpdt.tgz generation |
Sat, 13 Sep 2008 14:31:51 -0400 |
Adam Chlipala |
Improve template generation; craft template for InductiveTypes |
Sat, 13 Sep 2008 08:58:48 -0400 |
Adam Chlipala |
Spell check |
Fri, 12 Sep 2008 17:18:11 -0400 |
Adam Chlipala |
Publishing to the web |
Fri, 12 Sep 2008 16:55:37 -0400 |
Adam Chlipala |
Exercises |
Fri, 12 Sep 2008 15:30:59 -0400 |
Adam Chlipala |
TVL and constant-folding exercises |
Fri, 12 Sep 2008 14:59:08 -0400 |
Adam Chlipala |
Manual Proofs About Constructors |
Wed, 10 Sep 2008 15:47:22 -0400 |
Adam Chlipala |
Nested Inductive Types |
Wed, 10 Sep 2008 14:41:41 -0400 |
Adam Chlipala |
Interlude on Proof Terms |
Wed, 10 Sep 2008 12:54:51 -0400 |
Adam Chlipala |
Reflexive Types |
Wed, 10 Sep 2008 12:16:54 -0400 |
Adam Chlipala |
Little fixes |
Mon, 08 Sep 2008 16:00:02 -0400 |
Adam Chlipala |
Mutual induction |
Mon, 08 Sep 2008 15:38:34 -0400 |
Adam Chlipala |
Parameterized inductives |
Mon, 08 Sep 2008 15:23:04 -0400 |
Adam Chlipala |
nat lists and trees |
Mon, 08 Sep 2008 15:02:18 -0400 |
Adam Chlipala |
nat |
Mon, 08 Sep 2008 14:28:55 -0400 |
Adam Chlipala |
bool |
Mon, 08 Sep 2008 14:19:50 -0400 |
Adam Chlipala |
Start of Inductive Types |
Mon, 08 Sep 2008 12:42:57 -0400 |
Adam Chlipala |
Real chapter titles; describe how to get Proof General to use command-line flags |
Mon, 08 Sep 2008 12:22:22 -0400 |
Adam Chlipala |
Fix Makefile 'doc' target |
Fri, 05 Sep 2008 16:48:13 -0400 |
Adam Chlipala |
Switch [input_line] to [read_line] |
Fri, 05 Sep 2008 16:46:32 -0400 |
Adam Chlipala |
Template generation |
Wed, 03 Sep 2008 16:37:51 -0400 |
Adam Chlipala |
Proper title and copyright pages |
Wed, 03 Sep 2008 16:14:47 -0400 |
Adam Chlipala |
Finished typed example |
Wed, 03 Sep 2008 15:59:37 -0400 |
Adam Chlipala |
Translation |
Wed, 03 Sep 2008 15:39:41 -0400 |
Adam Chlipala |
Typed target denotation |
Wed, 03 Sep 2008 15:08:28 -0400 |
Adam Chlipala |
Target language source examples |
Wed, 03 Sep 2008 15:05:21 -0400 |
Adam Chlipala |
Source language examples |
Wed, 03 Sep 2008 15:00:56 -0400 |
Adam Chlipala |
Source language semantics |
Wed, 03 Sep 2008 14:26:52 -0400 |
Adam Chlipala |
Typed expression language |
Wed, 03 Sep 2008 13:45:59 -0400 |
Adam Chlipala |
Merge; make prose nicer |
Wed, 03 Sep 2008 13:30:05 -0400 |
Adam Chlipala |
Squash book into main directory |
Mon, 01 Sep 2008 12:52:30 -0400 |
Adam Chlipala |
Nats StackMachine done |
Mon, 01 Sep 2008 11:30:27 -0400 |
Adam Chlipala |
Target language and translation |
Mon, 01 Sep 2008 11:18:58 -0400 |
Adam Chlipala |
Stack Machine initial source language |
Mon, 01 Sep 2008 10:25:40 -0400 |
Adam Chlipala |
First cut at Intro done |
Mon, 01 Sep 2008 10:00:09 -0400 |
Adam Chlipala |
Why not Agda/Epigram? |
Mon, 01 Sep 2008 09:27:25 -0400 |
Adam Chlipala |
Placeholders to create html and latex directories |
Fri, 29 Aug 2008 17:20:57 -0400 |
Adam Chlipala |
More of Intro |
Fri, 29 Aug 2008 16:41:49 -0400 |
Adam Chlipala |
Start of Intro |
Fri, 29 Aug 2008 14:24:38 -0400 |
Adam Chlipala |
Pretty LaTeX generation |
Fri, 29 Aug 2008 13:42:37 -0400 |
Adam Chlipala |
Start of stack machine example |
Wed, 20 Aug 2008 11:23:02 -0400 |
Adam Chlipala |
Possible class topics |
Wed, 20 Aug 2008 10:14:55 -0400 |
Adam Chlipala |
Syllabus prose |