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

Commit graph

  • 34f586559f SharedMemory: soundness of partial-order reduction (or one particular flavor thereof) Adam Chlipala 2016-04-24 13:56:33 -0400
  • 50baaa91fe SharedMemory: for partial-order reduction, only admit left uses the crucial commutativity property Adam Chlipala 2016-04-24 13:01:16 -0400
  • ec5df8f782 SharedMemory: proved the easier case of step->stepC Adam Chlipala 2016-04-24 08:30:25 -0400
  • 606efc383d SharedMemory: formulated a strategy for proving partial-order reduction, based on completing each trace to a stuck state Adam Chlipala 2016-04-23 21:09:53 -0400
  • 3b7d898b0f SharedMemory: commutes_sound Adam Chlipala 2016-04-22 19:11:42 -0400
  • 784c89332d SharedMemory: independent_threads Adam Chlipala 2016-04-22 18:25:07 -0400
  • ec5a4a198e SharedMemory: change StepParProceed Adam Chlipala 2016-04-22 17:58:14 -0400
  • e9849b9e9c SharedMemory: stronger notAboutToFail Adam Chlipala 2016-04-21 20:35:34 -0400
  • a8a8ff0bc6 SharedMemory: first optimization Adam Chlipala 2016-04-21 19:12:02 -0400
  • f37e9ba34d SharedMemory: model-checking example, after tweaking library Adam Chlipala 2016-04-21 13:42:30 -0400
  • 3e4e48c0eb SharedMemory: first cut at operational semantics Adam Chlipala 2016-04-21 10:28:08 -0400
  • c159847851 SeparationLogic: remove some unneeded definitions Adam Chlipala 2016-04-21 10:18:13 -0400
  • 28bd2266bf SeparationLogic_template Adam Chlipala 2016-04-20 10:29:55 -0400
  • 47fd9a8abf SepCancel: adapt for Coq versions Adam Chlipala 2016-04-20 08:36:48 -0400
  • 2dc04da2b9 SeparationLogic chapter: a pass through Adam Chlipala 2016-04-19 23:23:34 -0400
  • 5bc113f01d SeparationLogic chapter: soundness proof Adam Chlipala 2016-04-19 23:08:38 -0400
  • 3ddafb3b3a SeparationLogic chapter: program logic Adam Chlipala 2016-04-19 22:51:56 -0400
  • 4243295d81 Start of SeparationLogic chapter: assertion logic Adam Chlipala 2016-04-19 22:18:54 -0400
  • f6c7c2a482 Start of SeparationLogic chapter: object language Adam Chlipala 2016-04-19 21:45:52 -0400
  • 4209399eb1 Comment SeparationLogic, while getting it working with Coq 8.4 Adam Chlipala 2016-04-19 21:25:39 -0400
  • c9d7a69287 SepCancel: now less conservative Adam Chlipala 2016-04-19 19:16:14 -0400
  • 60c21c07ec SepCancel: be more cautious in a few ways Adam Chlipala 2016-04-19 18:36:25 -0400
  • 68b01b1047 Add SepCancel to 'lib' target Adam Chlipala 2016-04-19 14:29:02 -0400
  • e1844abf25 Factor out SepCancel Adam Chlipala 2016-04-19 14:28:30 -0400
  • 3261ad2809 SeparationLogic: change HtFree to make automation easier Adam Chlipala 2016-04-18 14:05:13 -0400
  • 63be3681c8 SeparationLogic: example verifications Adam Chlipala 2016-04-17 21:49:48 -0400
  • ef310e2b1e SeparationLogic: soundness proof Adam Chlipala 2016-04-17 16:55:52 -0400
  • 9dc96733d4 SeparationLogic: object language Adam Chlipala 2016-04-17 13:36:25 -0400
  • 1de08dee66 Embeddings chapter finished Adam Chlipala 2016-04-11 10:22:03 -0400
  • 455163b5f7 Embeddings chapter: first Hoare logic Adam Chlipala 2016-04-11 09:46:29 -0400
  • 477113cf40 Start of embeddings chapter Adam Chlipala 2016-04-11 09:24:35 -0400
  • cf003490a2 DeepAndShallowEmbedding_template Adam Chlipala 2016-04-11 08:30:17 -0400
  • 145bff88c6 DeepAndShallowEmbeddings: Coq 8.4 support Adam Chlipala 2016-04-11 08:13:49 -0400
  • e50cbae0c3 DeepAndShallowEmbeddings: comments Adam Chlipala 2016-04-10 19:50:20 -0400
  • 7a49ce887f DeepAndShallowEmbeddings: initial, simpler example Adam Chlipala 2016-04-10 18:53:36 -0400
  • 11e1c74b1c DeepAndShallowEmbeddings: proof automation for examples Adam Chlipala 2016-04-10 17:01:03 -0400
  • 4849bf22a2 DeepAndShallowEmbeddings: example of a derived program form Adam Chlipala 2016-04-10 16:33:32 -0400
  • 9330f3714e DeepAndShallowEmbeddings: adding failure Adam Chlipala 2016-04-10 15:38:47 -0400
  • 290fec1e5b DeepAndShallowEmbeddings: Deep Adam Chlipala 2016-04-10 15:10:56 -0400
  • 01d550e4b0 DeepAndShallowEmbeddings: ran some code in OCaml Adam Chlipala 2016-04-10 13:48:58 -0400
  • d5c82fa62e Three new axioms in Map Adam Chlipala 2016-03-29 13:15:17 -0400
  • bd17945c3a Add new chapter to README Adam Chlipala 2016-03-29 08:57:56 -0400
  • b9e4f4f131 HoareLogic chapter: transition-system invariants Adam Chlipala 2016-03-27 20:42:02 -0400
  • ecb0e87251 HoareLogic chapter: small-step semantics Adam Chlipala 2016-03-27 20:24:35 -0400
  • d77c6a96b2 HoareLogic chapter: soundness Adam Chlipala 2016-03-27 20:03:54 -0400
  • 647021bfb7 HoareLogic chapter: big-step semantics Adam Chlipala 2016-03-27 19:09:47 -0400
  • 91693e4f0f HoareLogic: comments Adam Chlipala 2016-03-27 18:44:35 -0400
  • a180698487 HoareLogic: yet another way to prove an invariant of a transition system Adam Chlipala 2016-03-27 15:33:27 -0400
  • c8e3a3fdcd Start HoareLogic, with several examples Adam Chlipala 2016-03-27 14:44:22 -0400
  • d9c5173720 TypesAndMutation chapter: proofreading pass Adam Chlipala 2016-03-25 17:53:11 -0400
  • 149eccac8c TypesAndMutation chapter: garbage collection Adam Chlipala 2016-03-25 17:36:17 -0400
  • 2fde1182e9 TypesAndMutation chapter: type-safety proof Adam Chlipala 2016-03-25 16:55:31 -0400
  • f0b782b059 Start of TypesAndMutation chapter Adam Chlipala 2016-03-25 15:54:40 -0400
  • 927d17d04d A fix for Coq 8.4 Adam Chlipala 2016-03-25 13:22:16 -0400
  • f76a1055d8 TypesAndMutation: a diverging term Adam Chlipala 2016-03-24 11:24:14 -0400
  • ff42602069 TypesAndMutation: comments Adam Chlipala 2016-03-24 10:52:05 -0400
  • 0845fa85b4 TypesAndMutation: type safety with garbage collection Adam Chlipala 2016-03-24 10:24:54 -0400
  • 48e75a5ab5 Merge branch 'master' of ssh://schizomaniac.net//home/adamc/git-root/frap Adam Chlipala 2016-03-24 09:07:59 -0400
  • 90e194c27e Map.restrict Adam Chlipala 2016-03-24 08:28:53 -0400
  • cf9062fa4e TypesAndMutation: finish lambda-ref soundness proof Adam Chlipala 2016-03-22 14:17:40 -0400
  • c279d3d610 Start of type-safety proof for lambda calculus with references Adam Chlipala 2016-03-21 18:48:01 -0400
  • af77717e4f Update README with new chapter Adam Chlipala 2016-03-16 11:25:39 -0400
  • 8e6b5b8996 LambdaCalculusAndTypeSoundness_template Adam Chlipala 2016-03-14 13:14:41 -0400
  • 0fe16514a4 Change some tactics to use their usual names in the book code Adam Chlipala 2016-03-13 21:15:03 -0400
  • 8f0c986a00 Finished LambdaCalculus chapter Adam Chlipala 2016-03-13 21:11:51 -0400
  • 01aab3d04e LambdaCalculus chapter: small-step semantics Adam Chlipala 2016-03-13 20:12:56 -0400
  • b3692b97a5 LambdaCalculus chapter: a nonterminating lambda term Adam Chlipala 2016-03-13 19:52:46 -0400
  • 6367baba66 LambdaCalculus chapter: Church numerals Adam Chlipala 2016-03-13 19:46:28 -0400
  • d940a48b58 Start of LambdaCalculus book chapter Adam Chlipala 2016-03-13 19:14:53 -0400
  • ec261d542c Comment LambdaCalculusAndTypeSoundness Adam Chlipala 2016-03-13 15:17:09 -0400
  • a36ebc7802 LambdaCalculusAndTypeSoundness: Church numerals Adam Chlipala 2016-03-13 14:44:41 -0400
  • 55257f669d LambdaCalculusAndTypeSoundness: untyped lambda calculus semantics, two ways Adam Chlipala 2016-03-13 13:47:25 -0400
  • 9ce653261c LambdaCalculusAndTypeSoundness: a more manual soundness proof Adam Chlipala 2016-03-13 11:54:38 -0400
  • 23955eb536 Start LambdaCalculusAndTypeSoundness: automated soundness proof Adam Chlipala 2016-03-13 11:34:06 -0400
  • 5ed670b5a6 Merge pull request #12 from ZiyaoWei/patch-2 Adam Chlipala 2016-03-09 11:12:23 -0500
  • eba6dc15d2 Typo - invariant should be AnswerIs(n_0!) WZY 2016-03-09 11:02:24 -0500
  • a2c453c075 Merge pull request #11 from ZiyaoWei/patch-1 Adam Chlipala 2016-03-08 11:52:57 -0500
  • 0aac2cbdda Fix compiler for stack machine WZY 2016-03-08 09:49:27 -0500
  • 971075850b A few book fixes Adam Chlipala 2016-03-08 09:18:57 -0500
  • c9cedde15f Add AbstractInterpret; fix 8.4 compatibility Adam Chlipala 2016-03-07 18:49:16 -0500
  • 3657865469 Flip vertical order of prime-factors example Adam Chlipala 2016-03-07 07:51:40 -0500
  • 4607e1cd18 AbstractInterpretation chapter: widening Adam Chlipala 2016-03-06 23:36:54 -0500
  • 8d7913afa9 AbstractInterpretation chapter: flow-sensitive analysis Adam Chlipala 2016-03-06 22:45:47 -0500
  • d4b85c5f13 AbstractInterpretation chapter: flow-insensitive analysis Adam Chlipala 2016-03-06 22:06:31 -0500
  • 21999625ea Start of AbstractInterpretation book chapter Adam Chlipala 2016-03-06 21:20:20 -0500
  • 70974db013 Comment AbstractInterpretation Adam Chlipala 2016-03-06 20:30:05 -0500
  • 0b204ccdad AbstractInterpretation: applied widening with intervals Adam Chlipala 2016-03-05 22:54:52 -0500
  • e146afebe5 AbstractInterpretation: analyzed one example used intervals Adam Chlipala 2016-03-05 22:02:27 -0500
  • b2de37b496 AbstractInterpretation: interval_sound Adam Chlipala 2016-03-05 21:34:15 -0500
  • c568a047cd AbstractInterpretation: flow-insensitive analysis Adam Chlipala 2016-03-05 18:36:39 -0500
  • 062119d6a2 AbstractInterpretation: more even-odd examples Adam Chlipala 2016-03-05 16:47:13 -0500
  • 5ae0e6641e AbstractInterpretation: optimized execution engine some more, finishing loopy Adam Chlipala 2016-03-05 16:34:45 -0500
  • 2068f7691a Moved some AbstractInterpretation working code into library Adam Chlipala 2016-03-05 16:07:11 -0500
  • c303dc02c9 AbstractInterpretation: analyzed one program Adam Chlipala 2016-03-05 15:56:15 -0500
  • e892c8dbab AbstractInterpretation: proved a simulation and started using it Adam Chlipala 2016-03-05 15:17:41 -0500
  • d0d6b87a1d More on AbstractInterpretation example; need to do a proper abstraction into a new trsys Adam Chlipala 2016-03-04 16:14:41 -0500
  • 26023bdcb1 Start of AbstractInterpretation: interpret_sound Adam Chlipala 2016-03-04 14:00:34 -0500
  • e06af75c78 Add Imp, recapping OperationalSemantics object language and semantics Adam Chlipala 2016-03-04 12:49:08 -0500
  • 96327eb9aa OperationalSemantics_template (really this time) Adam Chlipala 2016-02-29 09:29:55 -0500
  • c4d622f7a1 OperationalSemantics_template Adam Chlipala 2016-02-29 09:03:15 -0500