pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-20 04:07:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
315 commits 1 branch 0 tags 1.6 MiB
Commit graph

315 commits

This branch
This branch
All branches
Author SHA1 Message Date
Adam Chlipala
db0f87d654 DeepAndShallowEmbeddings: comment typo fix 2017-04-24 09:28:48 -04:00
Adam Chlipala
a6624bdcf2 Typo fix in book 2017-04-18 21:01:12 -04:00
Adam Chlipala
9928399f5c Small typo fix in Chapter 11 2017-04-09 09:40:31 -04:00
Adam Chlipala
d8e580b331 DependentInductiveTypes 2017-04-02 20:50:10 -04:00
Adam Chlipala
e204041ff8 Tiny revisions to LambdaCalculusAndTypeSoundness 2017-04-02 19:18:34 -04:00
Adam Chlipala
119996a90c SubsetTypes_template 2017-03-22 09:15:33 -04:00
Adam Chlipala
31b0b6e9e5 SubsetTypes_template 2017-03-22 09:15:22 -04:00
Adam Chlipala
e9e8e6b92b Add two library lemmas 2017-03-21 21:39:37 -04:00
Adam Chlipala
c5600db874 SubsetTypes 2017-03-21 19:27:36 -04:00
Adam Chlipala
88df5601f5 CompilerCorrectness_template 2017-03-19 20:09:48 -04:00
Adam Chlipala
5df1caf940 CompilerCorrectness chapter: proofreading 2017-03-19 18:39:05 -04:00
Adam Chlipala
cefe711466 CompilerCorrectness chapter: simulation with multiple matching steps 2017-03-19 18:21:30 -04:00
Adam Chlipala
6c1af44f95 CompilerCorrectness chapter: simulation with skipping, after adding termination as an observable 2017-03-19 18:07:21 -04:00
Adam Chlipala
9974e130f0 CompilerCorrectness chapter: basic simulation and constant folding 2017-03-19 16:36:04 -04:00
Adam Chlipala
882c6868ec Start of CompilerCorrectness chapter: trace equivalence 2017-03-19 16:07:07 -04:00
Adam Chlipala
b11fede54e CompilerCorrectness: comments and a medium-size simplification of flattening 2017-03-19 15:27:40 -04:00
Adam Chlipala
dd7ce9f869 CompilerCorrectness: a running example program to optimize 2017-03-19 14:29:56 -04:00
Adam Chlipala
7cebd4bfba CompilerCorrectness: flatten_ok 2017-03-19 14:04:51 -04:00
Adam Chlipala
c4be95afab CompilerCorrectness: simulation_multiple 2017-03-19 12:32:40 -04:00
Adam Chlipala
a9ba30076d Merge 2017-03-18 20:20:23 -04:00
Adam Chlipala
bf85fa5c2c CompilerCorrectness: cfold_ok, both directions 2017-03-18 17:22:12 -04:00
Adam Chlipala
829b6a4304 CompilerCorrectness: cfold_ok, in only one direction 2017-03-18 15:23:45 -04:00
Adam Chlipala
7c705bb2fb CompilerCorrectness: a new simulation condition to get trace equivalence for free 2017-03-18 14:50:55 -04:00
Adam Chlipala
2832696faa Start of CompilerCorrectness: cfoldExprs_ok 2017-03-18 14:42:13 -04:00
Adam Chlipala
f4f4a5a6ce Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap 2017-03-18 12:30:55 -04:00
Adam Chlipala
67ed8a4a63 LogicProgramming bonus: extending an automated-proof example to build a runnable witness finder 2017-03-18 12:30:50 -04:00
Adam Chlipala
ab51849203 Fix title in comments 2017-03-15 12:01:28 -04:00
Adam Chlipala
8030db0a17 LogicProgramming_template.v 2017-03-15 11:58:45 -04:00
Adam Chlipala
e047f2b67c LogicProgramming 2017-03-14 17:16:09 -04:00
Adam Chlipala
0e06d062d1 Tweak OperationalSemantics_template.v 2017-03-13 10:51:40 -04:00
Adam Chlipala
c8322773a4 Simplify sets in hypotheses, too 2017-03-12 21:27:59 -04:00
Adam Chlipala
89b1b74c7b ProofByReflection_template 2017-03-08 14:05:46 -05:00
Adam Chlipala
2334b84505 Added set simplifier to ProofByReflection 2017-03-08 11:50:29 -05:00
Adam Chlipala
38750f74a9 Import ProofByReflection from CPDT 2017-03-08 10:46:02 -05:00
Adam Chlipala
cd2a474d5d Fix a performance bug in model_check 2017-03-07 14:59:56 -05:00
Adam Chlipala
1c88de0f7d Tweak files for ModelChecking in class 2017-03-06 09:44:29 -05:00
Adam Chlipala
1e7c33f0a9 Optimizing tactics for faster state-space exploration 2017-03-05 20:46:53 -05:00
Adam Chlipala
ddeb7b25fa IntroToProofScripting_template 2017-03-01 14:14:59 -05:00
Adam Chlipala
79a4b02b4c IntroToProofScripting 2017-03-01 14:06:11 -05:00
Adam Chlipala
6ffd08411c Fix typo in a comment 2017-02-27 09:52:21 -05:00
Adam Chlipala
09dec13dd3 DataAbstraction_template 2017-02-21 09:15:33 -05:00
Adam Chlipala
b27e58f11e Bump chapter numbers in Coq code comments 2017-02-21 09:00:30 -05:00
Adam Chlipala
392c995970 Typo fix (#17) 2017-02-21 08:54:42 -05:00
Adam Chlipala
04492da28c DataAbstraction chapter: proofreading 2017-02-20 17:06:06 -05:00
Adam Chlipala
a20f757c17 DataAbstraction chapter: specialized implementations 2017-02-20 16:56:11 -05:00
Adam Chlipala
30d48a6139 DataAbstraction chapter: rep functions 2017-02-20 16:38:53 -05:00
Adam Chlipala
1898619404 DataAbstraction chapter: equivalence relations 2017-02-20 16:25:50 -05:00
Adam Chlipala
4056523a61 Start of DataAbstraction book chapter 2017-02-20 16:06:33 -05:00
Adam Chlipala
ef6cb8cb53 Comment DataAbstraction 2017-02-20 15:24:51 -05:00
Adam Chlipala
69f6acb514 Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap 2017-02-16 21:01:23 -05:00