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

• 7c705bb2fb CompilerCorrectness: a new simulation condition to get trace equivalence for free Adam Chlipala 2017-03-18 14:50:55 -0400
• 2832696faa Start of CompilerCorrectness: cfoldExprs_ok Adam Chlipala 2017-03-18 14:42:13 -0400
• f4f4a5a6ce Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap Adam Chlipala 2017-03-18 12:30:55 -0400
• 67ed8a4a63 LogicProgramming bonus: extending an automated-proof example to build a runnable witness finder Adam Chlipala 2017-03-18 12:30:50 -0400
• ab51849203 Fix title in comments Adam Chlipala 2017-03-15 12:01:28 -0400
• 8030db0a17 LogicProgramming_template.v Adam Chlipala 2017-03-15 11:58:45 -0400
• e047f2b67c LogicProgramming Adam Chlipala 2017-03-14 17:16:09 -0400
• 0e06d062d1 Tweak OperationalSemantics_template.v Adam Chlipala 2017-03-13 10:51:40 -0400
• c8322773a4 Simplify sets in hypotheses, too Adam Chlipala 2017-03-12 21:27:59 -0400
• 89b1b74c7b ProofByReflection_template Adam Chlipala 2017-03-08 14:05:46 -0500
• 2334b84505 Added set simplifier to ProofByReflection Adam Chlipala 2017-03-08 11:50:29 -0500
• 38750f74a9 Import ProofByReflection from CPDT Adam Chlipala 2017-03-08 10:44:25 -0500
• cd2a474d5d Fix a performance bug in model_check Adam Chlipala 2017-03-07 14:59:56 -0500
• 1c88de0f7d Tweak files for ModelChecking in class Adam Chlipala 2017-03-06 09:44:29 -0500
• 1e7c33f0a9 Optimizing tactics for faster state-space exploration Adam Chlipala 2017-03-05 20:46:53 -0500
• ddeb7b25fa IntroToProofScripting_template Adam Chlipala 2017-03-01 14:14:59 -0500
• 79a4b02b4c IntroToProofScripting Adam Chlipala 2017-03-01 14:06:11 -0500
• 6ffd08411c Fix typo in a comment Adam Chlipala 2017-02-27 09:52:21 -0500
• 09dec13dd3 DataAbstraction_template Adam Chlipala 2017-02-21 09:15:33 -0500
• b27e58f11e Bump chapter numbers in Coq code comments Adam Chlipala 2017-02-21 09:00:30 -0500
• 392c995970 Typo fix (#17) Adam Chlipala 2017-02-21 08:54:42 -0500
• 04492da28c DataAbstraction chapter: proofreading Adam Chlipala 2017-02-20 17:06:06 -0500
• a20f757c17 DataAbstraction chapter: specialized implementations Adam Chlipala 2017-02-20 16:56:11 -0500
• 30d48a6139 DataAbstraction chapter: rep functions Adam Chlipala 2017-02-20 16:38:53 -0500
• 1898619404 DataAbstraction chapter: equivalence relations Adam Chlipala 2017-02-20 16:25:50 -0500
• 4056523a61 Start of DataAbstraction book chapter Adam Chlipala 2017-02-20 16:06:33 -0500
• ef6cb8cb53 Comment DataAbstraction Adam Chlipala 2017-02-20 15:24:51 -0500
• 69f6acb514 Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap Adam Chlipala 2017-02-16 21:01:23 -0500
• 6d6a7ade8b Merge branch 'master' of github.com:achlipala/frap Adam Chlipala 2017-02-16 21:01:09 -0500
• 975d2d5835 Fix filename in README Adam Chlipala 2017-02-16 17:33:56 -0500
• 643d44e524 Polymorphism: add a comment about the infamous quantifier-ordering issue with induction Adam Chlipala 2017-02-15 10:01:49 -0500
• cf4d06c222 DataAbstraction: range sets Adam Chlipala 2017-02-12 17:49:30 -0500
• f14ed26afa DataAbstraction: FindDuplicates Adam Chlipala 2017-02-12 16:27:57 -0500
• d09f1abe92 Start of DataAbstraction: finite sets Adam Chlipala 2017-02-12 15:54:34 -0500
• 0b7b299fb8 Start of DataAbstraction: queues with rep functions Adam Chlipala 2017-02-12 15:39:42 -0500
• 2dac252854 Start of DataAbstraction: queue examples Adam Chlipala 2017-02-12 15:19:48 -0500
• fed5f5d812 Correct filename in README Adam Chlipala 2017-02-09 13:54:58 -0500
• 1b97418f5e Polymorphism template Adam Chlipala 2017-02-09 13:51:16 -0500
• 849b547c2d Polymorphism: syntax trees Adam Chlipala 2017-02-09 13:39:12 -0500
• 0e32a409d7 Polymorphism: trees Adam Chlipala 2017-02-09 12:54:27 -0500
• b13baac51e Polymorphism: [zip] and [unzip] Adam Chlipala 2017-02-09 12:43:20 -0500
• b89cb28352 Start of Polymorphism Adam Chlipala 2017-02-09 12:25:45 -0500
• 0e74bcf948 Push the last code change through a further copy-and-paste instance Adam Chlipala 2017-02-09 06:58:38 -0500
• 6bcaa20632 Update book index page for this semester Adam Chlipala 2017-02-08 08:47:18 -0500
• 0e68042f07 Fix for Coq 8.5 again Adam Chlipala 2017-02-07 21:35:23 -0500
• 466ea72b27 Finish port to Coq 8.6 Adam Chlipala 2017-02-07 20:51:13 -0500
• 1768aa6ea7 Progress on porting to Coq 8.6 Adam Chlipala 2017-02-07 18:51:05 -0500
• 4b3e4abb58 Small typo fix in BasicSyntax Adam Chlipala 2017-02-07 15:11:54 -0500
• 2f1b363c4e Typo fixes in Chapter 2 Adam Chlipala 2017-02-07 14:49:38 -0500
• 18fa1370cf Typo fix (issue #15) Adam Chlipala 2016-12-31 14:04:08 -0500
• 534c925d4d Spellcheck Adam Chlipala 2016-12-31 13:58:33 -0500
• 050f5fbf82 Address typo reports and other suggestions from Eric Tanter Adam Chlipala 2016-12-31 13:53:50 -0500
• 84791f343f Typo fix (issue #14) Adam Chlipala 2016-10-12 13:24:52 -0400
• ee4aec520b Correct definition of reachability Adam Chlipala 2016-10-11 14:36:26 -0400
• e3128435f8 Typo fix in comment Adam Chlipala 2016-09-22 07:55:45 -0400
• 2354de6eca Merge pull request #13 from ichung/typo Adam Chlipala 2016-06-30 14:13:41 -0400
• 672e072072 fix typo Istvan Chung 2016-06-29 13:25:48 -0400
• ea371df876 Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap Adam Chlipala 2016-05-15 14:41:01 -0400
• 6dcf4c1fa7 Fix two typos reported by dmz Adam Chlipala 2016-05-15 14:40:57 -0400
• 5455be7079 MessagesAndRefinement: Coq 8.4 compatibility Adam Chlipala 2016-05-09 10:42:13 -0400
• 15a5235792 MessagesAndRefinement: add to README Adam Chlipala 2016-05-08 19:00:15 -0400
• 254f370544 MessagesAndRefinement chapter: a pass through it all Adam Chlipala 2016-05-08 18:59:36 -0400
• 6333420f53 MessagesAndRefinement chapter: more algebraic laws Adam Chlipala 2016-05-08 18:43:27 -0400
• 97e672a323 MessagesAndRefinement chapter: refinement Adam Chlipala 2016-05-08 18:16:59 -0400
• c48cf684b0 MessagesAndRefinement chapter: object-language definition Adam Chlipala 2016-05-08 17:47:43 -0400
• 7a864f14df MessagesAndRefinement: comments Adam Chlipala 2016-05-08 16:58:41 -0400
• fdc5d2dee2 MessagesAndRefinement: gratuitous_composition_expanded Adam Chlipala 2016-05-08 15:56:15 -0400
• 012a3cc78a MessagesAndRefinement: gratuitous_composition Adam Chlipala 2016-05-08 09:24:00 -0400
• 9806321af1 MessagesAndRefinement: refines_add2_with_tester Adam Chlipala 2016-05-07 21:43:06 -0400
• 137121dcdc MessagesAndRefinement: refines_Par Adam Chlipala 2016-05-07 21:25:37 -0400
• db7a355195 MessagesAndRefinement: refines_Dup Adam Chlipala 2016-05-07 19:22:12 -0400
• 86516a58ec MessagesAndRefinement: add2_once_refines_simple_addN_once Adam Chlipala 2016-05-07 18:50:04 -0400
• d18dc3044e MessagesAndRefinement: trace refinement Adam Chlipala 2016-05-04 15:52:42 -0400
• c3935ce842 MessagesAndRefinement: base syntax and semantics Adam Chlipala 2016-05-04 15:29:34 -0400
• 1cb930d8d1 Fixes for Coq 8.4 Adam Chlipala 2016-05-01 20:09:39 -0400
• daac5734b0 Finalizing ConcurrentSeparationLogic Adam Chlipala 2016-05-01 19:45:51 -0400
• 035bfa57ee Make SepCancel more conservative Adam Chlipala 2016-05-01 18:53:25 -0400
• 8c67fc5468 ConcurrentSeparationLogic chapter: proofreading Adam Chlipala 2016-04-29 17:37:17 -0400
• 2f1d28a36a ConcurrentSeparationLogic chapter: soundness proof Adam Chlipala 2016-04-29 13:54:58 -0400
• 66ba12e539 ConcurrentSeparationLogic chapter: object language and program logic Adam Chlipala 2016-04-29 12:58:23 -0400
• f933a3ceab ConcurrentSeparationLogic: comments Adam Chlipala 2016-04-29 11:16:50 -0400
• 320eb45126 ConcurrentSeparationLogic: 3-stage producer-consumer Adam Chlipala 2016-04-28 10:20:16 -0400
• 6e80356fed ConcurrentSeparationLogic: more automation in examples Adam Chlipala 2016-04-28 10:07:43 -0400
• a242a93a7e ConcurrentSeparationLogic: a producer-consumer example (after tweaking SepCancel) Adam Chlipala 2016-04-28 10:03:10 -0400
• c335550a77 ConcurrentSeparationLogic: first example Adam Chlipala 2016-04-28 09:16:42 -0400
• 38d4e24966 ConcurrentSeparationLogic.v: finished soundness proof Adam Chlipala 2016-04-27 19:54:51 -0400
• 856d8b43b2 ConcurrentSeparationLogic: for soundness proof, only cases left are for unlock and parallel composition Adam Chlipala 2016-04-27 18:04:39 -0400
• de4b8fbec2 ConcurrentSeparationLogic: defined a program logic Adam Chlipala 2016-04-27 14:10:56 -0400
• e133afa3b8 Strengthen [sets] tactic Adam Chlipala 2016-04-26 20:52:39 -0400
• 132ac914e4 Sets: change parsing precedence Adam Chlipala 2016-04-26 13:46:48 -0400
• 512f585d90 SharedMemory: make work with Coq 8.5 Adam Chlipala 2016-04-25 09:00:28 -0400
• 4744a4039c SharedMemory chapter: proofreading Adam Chlipala 2016-04-24 22:19:03 -0400
• c60ec5864b SharedMemory chapter: proof of partial-order reduction Adam Chlipala 2016-04-24 21:23:46 -0400
• 5ee82091f7 SharedMemory chapter: local actions Adam Chlipala 2016-04-24 19:53:19 -0400
• 545f29c68d SharedMemory chapter: more on operational semantics Adam Chlipala 2016-04-24 19:26:29 -0400
• 592c7207bc SharedMemory chapter: operational semantics Adam Chlipala 2016-04-24 19:17:11 -0400
• 7675534511 SharedMemory: formatting cleanup Adam Chlipala 2016-04-24 15:31:34 -0400
• 9f938e6ac1 SharedMemory: comments Adam Chlipala 2016-04-24 15:29:21 -0400
• 8d250037e7 SharedMemory: prove that our running-time bound relation is not total Adam Chlipala 2016-04-24 14:38:05 -0400
• 9de4dbdebe SharedMemory: model-checked a concrete program with partial-order reduction Adam Chlipala 2016-04-24 14:29:28 -0400