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

440 commits

This branch
This branch
All branches
Author SHA1 Message Date
Adam Chlipala
ee4aec520b Correct definition of reachability 2016-10-11 14:36:26 -04:00
Adam Chlipala
e3128435f8 Typo fix in comment 2016-09-22 07:55:45 -04:00
Adam Chlipala
2354de6eca Merge pull request #13 from ichung/typo 
fix typo
 2016-06-30 14:13:41 -04:00
Istvan Chung
672e072072 fix typo 2016-06-29 13:25:48 -04:00
Adam Chlipala
ea371df876 Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap 2016-05-15 14:41:01 -04:00
Adam Chlipala
6dcf4c1fa7 Fix two typos reported by dmz 2016-05-15 14:40:57 -04:00
Adam Chlipala
5455be7079 MessagesAndRefinement: Coq 8.4 compatibility 2016-05-09 10:42:13 -04:00
Adam Chlipala
15a5235792 MessagesAndRefinement: add to README 2016-05-08 19:00:15 -04:00
Adam Chlipala
254f370544 MessagesAndRefinement chapter: a pass through it all 2016-05-08 18:59:36 -04:00
Adam Chlipala
6333420f53 MessagesAndRefinement chapter: more algebraic laws 2016-05-08 18:43:27 -04:00
Adam Chlipala
97e672a323 MessagesAndRefinement chapter: refinement 2016-05-08 18:16:59 -04:00
Adam Chlipala
c48cf684b0 MessagesAndRefinement chapter: object-language definition 2016-05-08 17:47:43 -04:00
Adam Chlipala
7a864f14df MessagesAndRefinement: comments 2016-05-08 16:58:41 -04:00
Adam Chlipala
fdc5d2dee2 MessagesAndRefinement: gratuitous_composition_expanded 2016-05-08 15:56:15 -04:00
Adam Chlipala
012a3cc78a MessagesAndRefinement: gratuitous_composition 2016-05-08 09:24:00 -04:00
Adam Chlipala
9806321af1 MessagesAndRefinement: refines_add2_with_tester 2016-05-07 21:43:06 -04:00
Adam Chlipala
137121dcdc MessagesAndRefinement: refines_Par 2016-05-07 21:25:37 -04:00
Adam Chlipala
db7a355195 MessagesAndRefinement: refines_Dup 2016-05-07 19:22:12 -04:00
Adam Chlipala
86516a58ec MessagesAndRefinement: add2_once_refines_simple_addN_once 2016-05-07 18:50:04 -04:00
Adam Chlipala
d18dc3044e MessagesAndRefinement: trace refinement 2016-05-04 15:52:42 -04:00
Adam Chlipala
c3935ce842 MessagesAndRefinement: base syntax and semantics 2016-05-04 15:29:34 -04: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
035bfa57ee Make SepCancel more conservative 2016-05-01 18:53:25 -04:00
Adam Chlipala
8c67fc5468 ConcurrentSeparationLogic chapter: proofreading 2016-04-29 17:37:17 -04:00
Adam Chlipala
2f1d28a36a ConcurrentSeparationLogic chapter: soundness proof 2016-04-29 13:54:58 -04:00
Adam Chlipala
66ba12e539 ConcurrentSeparationLogic chapter: object language and program logic 2016-04-29 12:58:23 -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
Adam Chlipala
e133afa3b8 Strengthen [sets] tactic 2016-04-26 20:52:39 -04:00
Adam Chlipala
132ac914e4 Sets: change parsing precedence 2016-04-26 13:46:48 -04:00
Adam Chlipala
512f585d90 SharedMemory: make work with Coq 8.5 2016-04-25 09:00:28 -04:00
Adam Chlipala
4744a4039c SharedMemory chapter: proofreading 2016-04-24 22:19:03 -04:00
Adam Chlipala
c60ec5864b SharedMemory chapter: proof of partial-order reduction 2016-04-24 21:23:46 -04:00
Adam Chlipala
5ee82091f7 SharedMemory chapter: local actions 2016-04-24 19:53:19 -04:00
Adam Chlipala
545f29c68d SharedMemory chapter: more on operational semantics 2016-04-24 19:26:29 -04:00
Adam Chlipala
592c7207bc SharedMemory chapter: operational semantics 2016-04-24 19:17:11 -04:00
Adam Chlipala
7675534511 SharedMemory: formatting cleanup 2016-04-24 15:31:34 -04:00
Adam Chlipala
9f938e6ac1 SharedMemory: comments 2016-04-24 15:29:21 -04:00
Adam Chlipala
8d250037e7 SharedMemory: prove that our running-time bound relation is not total 2016-04-24 14:38:05 -04:00
Adam Chlipala
9de4dbdebe SharedMemory: model-checked a concrete program with partial-order reduction 2016-04-24 14:29:28 -04:00
Adam Chlipala
34f586559f SharedMemory: soundness of partial-order reduction (or one particular flavor thereof) 2016-04-24 13:56:33 -04:00
Adam Chlipala
50baaa91fe SharedMemory: for partial-order reduction, only admit left uses the crucial commutativity property 2016-04-24 13:01:16 -04:00
Adam Chlipala
ec5df8f782 SharedMemory: proved the easier case of step->stepC 2016-04-24 08:30:25 -04:00