Sun, 26 Oct 2008 15:18:13 -0400 |
Adam Chlipala |
Functional programming in Ltac |
Sun, 26 Oct 2008 14:39:21 -0400 |
Adam Chlipala |
Free variables in unification variables issue |
Sun, 26 Oct 2008 14:11:41 -0400 |
Adam Chlipala |
Through completer' |
Sun, 26 Oct 2008 11:13:43 -0400 |
Adam Chlipala |
autorewrite |
Sun, 26 Oct 2008 10:28:00 -0400 |
Adam Chlipala |
auto |
Wed, 22 Oct 2008 14:32:41 -0400 |
Adam Chlipala |
Start of Match |
Wed, 22 Oct 2008 13:40:32 -0400 |
Adam Chlipala |
call-by-name is really call-by-need |
Wed, 22 Oct 2008 09:43:37 -0400 |
Adam Chlipala |
Clarify intent to use hlist |
Wed, 22 Oct 2008 07:50:47 -0400 |
Adam Chlipala |
s/reflexive/index function |
Mon, 20 Oct 2008 17:02:04 -0400 |
Adam Chlipala |
s/itree/htree |
Mon, 20 Oct 2008 14:03:08 -0400 |
Adam Chlipala |
Equality exercise |
Mon, 20 Oct 2008 12:17:39 -0400 |
Adam Chlipala |
More DepList notations |
Mon, 20 Oct 2008 10:44:20 -0400 |
Adam Chlipala |
Add ext_eq axiom and DepList notations |
Mon, 20 Oct 2008 09:11:54 -0400 |
Adam Chlipala |
Templatize Equality |
Sat, 18 Oct 2008 17:36:08 -0400 |
Adam Chlipala |
ext_eq |
Sat, 18 Oct 2008 15:32:59 -0400 |
Adam Chlipala |
Definitional equality |
Sat, 18 Oct 2008 14:55:52 -0400 |
Adam Chlipala |
Interconvertibility |
Sat, 18 Oct 2008 14:24:11 -0400 |
Adam Chlipala |
JMeq |
Sat, 18 Oct 2008 13:52:09 -0400 |
Adam Chlipala |
Proofs with equality |
Sat, 18 Oct 2008 12:04:28 -0400 |
Adam Chlipala |
Up to Streicher |
Tue, 14 Oct 2008 15:21:02 -0400 |
Adam Chlipala |
Clarify exercise wording |
Tue, 14 Oct 2008 15:11:14 -0400 |
Adam Chlipala |
Pattern-matching exercise |
Tue, 14 Oct 2008 14:58:33 -0400 |
Adam Chlipala |
itree exercise |
Tue, 14 Oct 2008 14:49:51 -0400 |
Adam Chlipala |
DepList |
Tue, 14 Oct 2008 13:05:43 -0400 |
Adam Chlipala |
Templatize DataStruct |
Tue, 14 Oct 2008 11:28:44 -0400 |
Adam Chlipala |
Commentary on cond example |
Tue, 14 Oct 2008 10:52:38 -0400 |
Adam Chlipala |
Code for cond-folding example |
Mon, 13 Oct 2008 15:09:58 -0400 |
Adam Chlipala |
Index functions |
Mon, 13 Oct 2008 14:04:39 -0400 |
Adam Chlipala |
Recursive type definitions |
Mon, 13 Oct 2008 13:20:57 -0400 |
Adam Chlipala |
STLC interp |
Mon, 13 Oct 2008 12:35:48 -0400 |
Adam Chlipala |
hlist and hget |
Mon, 13 Oct 2008 11:59:20 -0400 |
Adam Chlipala |
Commentary on ilist get |
Mon, 13 Oct 2008 10:47:21 -0400 |
Adam Chlipala |
Start of DataStruct |
Sun, 12 Oct 2008 08:44:23 -0400 |
Adam Chlipala |
s/stream/tree |
Wed, 08 Oct 2008 14:22:47 -0400 |
Adam Chlipala |
Fix red-black section heading |
Wed, 08 Oct 2008 14:18:35 -0400 |
Adam Chlipala |
Add a darn newline |
Wed, 08 Oct 2008 13:55:20 -0400 |
Adam Chlipala |
Exercise added at end of MoreDep |
Wed, 08 Oct 2008 10:01:26 -0400 |
Adam Chlipala |
Templatize MoreDep |
Wed, 08 Oct 2008 09:41:50 -0400 |
Adam Chlipala |
crush' pursues trivial inversions |
Tue, 07 Oct 2008 22:14:39 -0400 |
Adam Chlipala |
Prettify rbtree a bit more |
Tue, 07 Oct 2008 22:05:37 -0400 |
Adam Chlipala |
Prettify rbtree a bit |
Tue, 07 Oct 2008 21:58:45 -0400 |
Adam Chlipala |
Move [present] section earlier |
Tue, 07 Oct 2008 21:49:35 -0400 |
Adam Chlipala |
Correctness of insertion |
Tue, 07 Oct 2008 20:15:12 -0400 |
Adam Chlipala |
Red-black insert |
Tue, 07 Oct 2008 16:50:46 -0400 |
Adam Chlipala |
Comment regexp matcher |
Tue, 07 Oct 2008 16:08:58 -0400 |
Adam Chlipala |
Finish automating regexp |
Tue, 07 Oct 2008 14:52:15 -0400 |
Adam Chlipala |
Add star to regexp matcher; need to automate a bit more |
Tue, 07 Oct 2008 10:50:36 -0400 |
Adam Chlipala |
Remove -impredicative-set from text |
Tue, 07 Oct 2008 10:49:07 -0400 |
Adam Chlipala |
Remove -impredicative-set |
Tue, 07 Oct 2008 10:43:54 -0400 |
Adam Chlipala |
Get Coinductive compiling again |
Mon, 06 Oct 2008 14:41:13 -0400 |
Adam Chlipala |
Add 'Or' to regexp matcher |
Mon, 06 Oct 2008 14:33:11 -0400 |
Adam Chlipala |
Start of certified regexp matcher |
Mon, 06 Oct 2008 13:07:24 -0400 |
Adam Chlipala |
Tagless interpreter & cfold |
Sun, 05 Oct 2008 20:07:35 -0400 |
Adam Chlipala |
Incorporate crush' bug reports; ilists in MoreDep |
Sun, 05 Oct 2008 15:42:14 -0400 |
Adam Chlipala |
Start of MoreDep |
Sun, 05 Oct 2008 12:12:19 -0400 |
Adam Chlipala |
Subset exercises |
Sun, 05 Oct 2008 11:34:09 -0400 |
Adam Chlipala |
Coinductive exercise description |
Sat, 04 Oct 2008 14:58:00 -0400 |
Adam Chlipala |
Try arithmetic contradiction |
Fri, 03 Oct 2008 17:53:41 -0400 |
Adam Chlipala |
Expand MoreSpecif |
Fri, 03 Oct 2008 15:59:59 -0400 |
Adam Chlipala |
MoreSpecif |
Fri, 03 Oct 2008 15:27:39 -0400 |
Adam Chlipala |
Templatizing Subset |
Fri, 03 Oct 2008 15:11:44 -0400 |
Adam Chlipala |
Spell check |
Fri, 03 Oct 2008 15:10:30 -0400 |
Adam Chlipala |
Type-checking example, with discussion |
Fri, 03 Oct 2008 14:29:21 -0400 |
Adam Chlipala |
Break into Parts |
Fri, 03 Oct 2008 14:14:28 -0400 |
Adam Chlipala |
maybe and sumor |
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 |