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

26 commits

Author SHA1 Message Date
Adam Chlipala
f3211734b9 A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
Adam Chlipala
f428750fdf Change notation to remain compatible with multiple Coq versions 2022-01-31 21:02:31 -05:00
Adam Chlipala
d745f0802e Ported to Coq 8.15 2022-01-29 15:13:09 -05:00
Adam Chlipala
8fdc4e2cfd Revising before this week's lectures 2021-05-10 10:45:34 -04:00
Adam Chlipala
75ea3ed0b3 Chapter renumbering 2021-03-28 17:03:56 -04:00
Adam Chlipala
d3c7a85b49 More cleanup around addition of RuleInduction 2021-03-01 12:15:34 -05:00
Adam Chlipala
d1d44e55f6 Small patch for Coq 8.13 2021-02-14 17:26:21 -05:00
Adam Chlipala
b7f248e099 ConcurrentSeparationLogic: stop bothering to choose postconditions for parallel compositions, which can't terminate (addresses #52) 2021-01-03 15:20:26 -05:00
Matthew Dempsky
509ebb1d06 Fix typo in ConcurrentSeparationLogic.v example 
In the 3-stage example, the middle stage moves list elements from the
first stack to the second stack, not back onto the first stack again.
 2020-09-24 13:30:58 -07:00
Adam Chlipala
5f735225ef Revising before class 2020-04-28 09:40:40 -04:00
Adam Chlipala
0f73a3901c Proofreading ConcurrentSeparationLogic 2018-05-08 09:13:06 -04:00
Adam Chlipala
a8239e7925 Commented ProgramDerivation, with chapter renumbering in Coq code 2018-05-06 12:53:49 -04:00
Adam Chlipala
369edcdd79 Update for new Connecting chapter, modulo adding the LaTeX content 2018-05-02 11:56:01 -04:00
Adam Chlipala
2832696faa Start of CompilerCorrectness: cfoldExprs_ok 2017-03-18 14:42:13 -04:00
Adam Chlipala
1e7c33f0a9 Optimizing tactics for faster state-space exploration 2017-03-05 20:46:53 -05:00
Adam Chlipala
b27e58f11e Bump chapter numbers in Coq code comments 2017-02-21 09:00:30 -05:00
Adam Chlipala
1cb930d8d1 Fixes for Coq 8.4 2016-05-01 20:09:39 -04:00
Adam Chlipala
daac5734b0 Finalizing ConcurrentSeparationLogic 2016-05-01 19:45:51 -04:00
Adam Chlipala
f933a3ceab ConcurrentSeparationLogic: comments 2016-04-29 11:16:50 -04:00
Adam Chlipala
320eb45126 ConcurrentSeparationLogic: 3-stage producer-consumer 2016-04-28 10:20:16 -04:00
Adam Chlipala
6e80356fed ConcurrentSeparationLogic: more automation in examples 2016-04-28 10:07:43 -04:00
Adam Chlipala
a242a93a7e ConcurrentSeparationLogic: a producer-consumer example (after tweaking SepCancel) 2016-04-28 10:03:10 -04:00
Adam Chlipala
c335550a77 ConcurrentSeparationLogic: first example 2016-04-28 09:16:42 -04:00
Adam Chlipala
38d4e24966 ConcurrentSeparationLogic.v: finished soundness proof 2016-04-27 19:54:51 -04:00
Adam Chlipala
856d8b43b2 ConcurrentSeparationLogic: for soundness proof, only cases left are for unlock and parallel composition 2016-04-27 18:04:39 -04:00
Adam Chlipala
de4b8fbec2 ConcurrentSeparationLogic: defined a program logic 2016-04-27 14:10:56 -04:00