Commit graph

Select branches

Hide pull requests

master

#10

#11

#12

#13

#19

#20

#21

#22

#22

#23

#25

#26

#29

#3

#3

#30

#31

#33

#34

#35

#36

#38

#39

#4

#4

#40

#42

#43

#44

#48

#50

#51

#53

#55

#56

#57

#61

#61

#8

#8

#9

#9

Mono Color

• 64516f784a Fix goofy notation Adam Chlipala 2016-02-28 20:18:29 -0500
• ce0d9e8262 Extend tactic reference and update README Adam Chlipala 2016-02-28 14:55:27 -0500
• bf825fea8b OperationalSemantics chapter done Adam Chlipala 2016-02-28 14:50:20 -0500
• f5685818a2 OperationalSemantics chapter: contextual Adam Chlipala 2016-02-28 14:19:45 -0500
• 3c929bd574 OperationalSemantics chapter: small-step Adam Chlipala 2016-02-28 13:40:21 -0500
• aff55e3796 Start of OperationalSemantics chapter: big-step Adam Chlipala 2016-02-28 13:00:10 -0500
• cad03f728d Comment OperationalSemantics Adam Chlipala 2016-02-28 12:25:15 -0500
• 31bb6daffb OperationalSemantics: Add concurrency example Adam Chlipala 2016-02-28 11:56:17 -0500
• 4889f08ac4 Avoid a notation conflict Adam Chlipala 2016-02-25 11:54:03 -0500
• a583e1d0d4 Fancier set simplification Adam Chlipala 2016-02-23 18:59:50 -0500
• 32ad7c8e8e Some tactic tweaks in preparation for Lab 3 Adam Chlipala 2016-02-23 15:23:16 -0500
• cff5e1da35 Merge pull request #10 from wangpengmit/pull-request-singletoner Adam Chlipala 2016-02-23 14:52:43 -0500
• f05378e111 Tweaked Ltac singletoner to display state space exploration in real time Peng Wang 2016-02-22 17:53:31 -0500
• cc19c1708b Add [parallel] to libary Adam Chlipala 2016-02-22 17:28:40 -0500
• 06b5592c89 Ignore .coq-native Adam Chlipala 2016-02-22 10:36:30 -0500
• 53bf09c416 ModelChecking_template Adam Chlipala 2016-02-22 09:45:53 -0500
• 65c56a7a2e Tweak model-checking library support Adam Chlipala 2016-02-21 17:00:01 -0500
• d677f255c4 OperationalSemantics: manually proved invariant and determinism Adam Chlipala 2016-02-21 15:01:24 -0500
• 72ac97a60a OperationalSemantics: automated contextual small-step Adam Chlipala 2016-02-21 13:55:18 -0500
• ab4420c66f OperationalSemantics: contextual small-step Adam Chlipala 2016-02-21 13:52:54 -0500
• 6e0b98c8b4 OperationalSemantics: a model-checking example Adam Chlipala 2016-02-21 13:39:22 -0500
• f67d9b5e32 OperationalSemantics: automated equivalence of big and small Adam Chlipala 2016-02-21 13:23:09 -0500
• 918fcaa29b OperationalSemantics: equivalence of big and small Adam Chlipala 2016-02-21 13:19:16 -0500
• db643cbfc4 Start of OperationalSemantics: big-step and factorial Adam Chlipala 2016-02-21 12:51:05 -0500
• fd45f9d71a Add ModelCheck Adam Chlipala 2016-02-21 12:16:31 -0500
• 4d54fe8857 Add to the tactic reference Adam Chlipala 2016-02-21 12:04:59 -0500
• 211ede66a0 ModelChecking chapter done Adam Chlipala 2016-02-21 11:26:24 -0500
• cbf2bb71fa ModelChecking chapter: abstracting a transition system Adam Chlipala 2016-02-21 10:12:17 -0500
• 353c853893 Start of ModelChecking chapter Adam Chlipala 2016-02-21 09:32:24 -0500
• 2b6ea9913c Comments for ModelChecking Adam Chlipala 2016-02-21 09:07:14 -0500
• 2c601b04a0 Fixed to work in Coq 8.4, too Adam Chlipala 2016-02-18 17:51:58 -0500
• cf65c18ebf A typo fix Adam Chlipala 2016-02-17 14:17:27 -0500
• 5f66f4f399 Add Chapter 4 code to README Adam Chlipala 2016-02-16 14:09:07 -0500
• 33d01606bf Harmonize inductive-definition convention Adam Chlipala 2016-02-16 11:41:30 -0500
• 0123f45d21 TransitionSystems_template Adam Chlipala 2016-02-16 11:29:08 -0500
• d04037a84f ModelChecking: an example of modularity Adam Chlipala 2016-02-16 11:17:50 -0500
• e3bb90c4a1 ModelChecking: another abstraction example Adam Chlipala 2016-02-16 08:03:25 -0500
• 7aa8e890cf ModelChecking: an example of abstraction Adam Chlipala 2016-02-15 21:20:54 -0500
• 218bb2fcf0 Add [first_order] Adam Chlipala 2016-02-15 19:39:36 -0500
• 53925f1a1f Renaming invariantFor_monotone to invariant_weaken Adam Chlipala 2016-02-15 18:59:39 -0500
• e669e53157 Reordering premises in Invariant theorems Adam Chlipala 2016-02-15 16:04:40 -0500
• 9b40bf78af New Makefile target: lib, to build just the library, not the lecture code Adam Chlipala 2016-02-14 22:07:29 -0500
• c129d8447e Some heftier ModelChecking examples Adam Chlipala 2016-02-14 19:23:26 -0500
• eb50f67c2a Smarter ModelChecking with a worklist Adam Chlipala 2016-02-14 17:55:59 -0500
• 4371d08696 Set simplification for ModelChecking Adam Chlipala 2016-02-14 17:33:46 -0500
• c88ae6d484 Start ModelChecking code: checked [factorial_sys] Adam Chlipala 2016-02-14 17:13:25 -0500
• c3182f3007 TransitionSystems chapter: first full draft Adam Chlipala 2016-02-14 15:00:49 -0500
• b2d23e8468 TransitionSystems chapter: rule induction Adam Chlipala 2016-02-14 13:51:11 -0500
• a93ae59e0b TransitionSystems chapter: invariants Adam Chlipala 2016-02-14 13:32:00 -0500
• 571aff7ad3 TransitionSystems chapter: factorial system Adam Chlipala 2016-02-14 12:59:25 -0500
• ef3f36933a TransitionSystems: code probably done Adam Chlipala 2016-02-14 12:25:48 -0500
• ee02d8926a TransitionSystems: factorial example finished Adam Chlipala 2016-02-14 11:41:41 -0500
• 9ae318190c Index to example source files for chapters Adam Chlipala 2016-02-13 19:45:22 -0500
• 40abba73e5 minor typos John Ankcorn 2016-02-11 09:36:10 -0500
• a0487bc153 Add Map remove Adam Chlipala 2016-02-09 22:44:03 -0500
• 19b98288ca Incorporating a variety of changes and pull requests, after things got desync'd a bit Adam Chlipala 2016-02-09 20:21:19 -0500
• c4bcf50fa8 Merge 555dc01231 into 9720a6e0c6 Theophilos Giannakopoulos 2016-02-10 00:33:50 +0000
• 555dc01231 Use Admitted instead of Qed when the proof contains "admit" to be compatible with Coq 8.5. Theophilos Giannakopoulos 2016-02-05 08:31:26 -0500
• ab85cc64ba Keep frap.tex from being clobbered on case-insensitive filesystems. Theophilos Giannakopoulos 2016-02-09 19:27:47 -0500
• 4539409e73 For Coq 8.5 compatibility, use [Admitted] instead of [admit] Adam Chlipala 2016-02-09 18:10:58 -0500
• 44696bb5b1 Beef up [equality] Adam Chlipala 2016-02-09 16:28:48 -0500
• 3ae5327314 Booleans and [propositional] Adam Chlipala 2016-02-09 13:11:58 -0500
• e4bdbbfbdf Merge Adam Chlipala 2016-02-09 09:07:57 -0500
• 087e9334d8 Rename [map] to [fmap] Adam Chlipala 2016-02-09 09:07:37 -0500
• 92e7e9d69d Merge 18f286bb38 into 9720a6e0c6 Mark Lemay 2016-02-09 02:00:42 +0000
• 18f286bb38 fixed a new line split Mark Lemay 2016-02-08 20:48:04 -0500
• 754784c286 TransitionSystems WIP Adam Chlipala 2016-02-08 18:14:11 -0500
• 3b82c0b2bd Start TransitionSystems code Adam Chlipala 2016-02-08 18:04:14 -0500
• 0734098643 Merge 99a7d8cd75 into 9720a6e0c6 Clément Pit--Claudel 2016-02-07 21:11:21 +0000
• 9720a6e0c6 One more redaction from Interpreters_template Adam Chlipala 2016-02-07 14:42:34 -0500
• 901cacd35a Add margin boxes to Interpreters Adam Chlipala 2016-02-07 14:28:06 -0500
• 5299d4ebf3 Add Interpreters_template Adam Chlipala 2016-02-07 14:23:54 -0500
• 583446eaf3 First full draft of Interpreter chapter Adam Chlipala 2016-02-07 11:43:25 -0500
• b947e838e0 Interpreter chapter: stack machine Adam Chlipala 2016-02-07 10:56:39 -0500
• 2134aa2477 Interpreter chapter: expressions and substitution Adam Chlipala 2016-02-07 10:25:40 -0500
• c8ff080a20 Add new Interpreter tactics to book appendix Adam Chlipala 2016-02-07 09:41:48 -0500
• c5ac90a5a9 Finished first version of Interpreters code Adam Chlipala 2016-02-07 09:39:40 -0500
• a73e085a0a Finish annotating factorial example in Interpreters Adam Chlipala 2016-02-07 09:14:13 -0500
• d13b70e0ee Add missing file to _CoqProject Adam Chlipala 2016-02-07 09:11:03 -0500
• fe8f0fb918 Finished annotating factorial example in Interpreters Adam Chlipala 2016-02-07 09:08:40 -0500
• 2645e91a23 Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap Adam Chlipala 2016-02-07 08:58:05 -0500
• ba3bb5c351 Interpreters: factorial example Adam Chlipala 2016-02-06 22:09:37 -0500
• 5e842c66f7 Start Interpreters code Adam Chlipala 2016-02-06 18:24:06 -0500
• 99a7d8cd75 Fix typo in 'arithmetic' Clément Pit--Claudel 2016-02-03 18:12:06 -0500
• 08f9417302 Added .dir-locals.el in .gitignore Peng Wang 2016-02-03 12:49:16 -0500
• 7c08f396d5 Pass over BasicSyntax, adding template Adam Chlipala 2016-02-03 08:39:24 -0500
• f946e0858c Start of appendix on Coq pragmatics Adam Chlipala 2016-02-02 15:38:24 -0500
• 1208d0cfd4 Tweak Makefile dependencies Adam Chlipala 2016-02-02 13:55:33 -0500
• 792a45b506 Tweak Makefile dependencies Adam Chlipala 2016-02-02 13:53:58 -0500
• 6f43dcc6de Tweak Makefile dependencies Adam Chlipala 2016-02-02 13:53:21 -0500
• 7e99e09b81 Publishing to web Adam Chlipala 2016-02-02 13:53:00 -0500
• 126f9a188d Export List Adam Chlipala 2016-02-02 12:38:00 -0500
• 48c8906d10 Proofreading pass through Chapter 2 Adam Chlipala 2016-01-31 22:19:34 -0500
• f39f2ab0d3 A first draft of Chapter 2 Adam Chlipala 2016-01-31 21:58:55 -0500
• e94795327d Finish commenting BasicSyntax Adam Chlipala 2016-01-31 20:16:24 -0500
• 99cc0af1a2 Commenting BasicSyntax Adam Chlipala 2016-01-31 19:51:59 -0500
• 42d48c6e58 More examples for first chapter Adam Chlipala 2016-01-16 20:32:12 -0500
• f8945106da Start of BasicSyntax code Adam Chlipala 2015-12-31 15:44:34 -0500
• e5898976ab Fleshed out intro Adam Chlipala 2015-12-31 14:40:01 -0500
• 2d64f99796 Placeholder introduction Adam Chlipala 2015-12-31 14:02:34 -0500