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

  • 8a87c209f7 Revising before class Adam Chlipala 2020-05-05 19:26:59 -0400
  • 1c91cf3d5c Merge branch 'master' of github.com:achlipala/frap Adam Chlipala 2020-04-29 16:06:34 -0400
  • c2bbf00999 Update for latest Coq version Adam Chlipala 2020-04-29 14:29:58 -0400
  • 5f735225ef Revising before class Adam Chlipala 2020-04-28 09:40:40 -0400
  • 300f78191e Revising before class Adam Chlipala 2020-04-26 14:30:18 -0400
  • 42d5af6d2d Revising before class Adam Chlipala 2020-04-26 14:29:53 -0400
  • 213f8b270b Revising before class Adam Chlipala 2020-04-26 14:28:52 -0400
  • e56390f108 Update SessionTypes to follow changes in MessagesAndRefinement Adam Chlipala 2020-04-24 11:15:51 -0400
  • a8dd970c96
         Merge pull request #44 from samuelgruetter/message_passing_fixes Adam Chlipala 2020-04-24 09:50:30 -0400
  • eccb504f08
         Merge pull request #43 from bkushigian/master Adam Chlipala 2020-04-24 09:29:23 -0400
  • 26b8436e0c fix warnings in MessagesAndRefinement.v Samuel Gruetter 2020-04-21 19:22:39 -0400
  • ceddf6d6e4 the few keystrokes saved by using a Coercion from action Samuel Gruetter 2020-04-21 19:19:18 -0400
  • 6a1e7fa644 also replace Set by Type in LStepSend and LStepRecv Samuel Gruetter 2020-04-20 21:42:33 -0400
  • 22f3238a8a Change overloaded term S in section 5.4 bkushigian 2020-04-20 09:34:30 -0700
  • 69de20dec8 Revising before class, including with an optimization to the model-checking engine Adam Chlipala 2020-04-20 11:56:23 -0400
  • c607913898 Typo in translation rule Adam Chlipala 2020-04-15 09:48:24 -0400
  • d74a0ebb42 Revising before class Adam Chlipala 2020-04-14 15:48:36 -0400
  • 2efec7b61d Typo fix Adam Chlipala 2020-04-14 11:55:26 -0400
  • ce1bc740c4 allow Type instead of just Set in Send and Recv Samuel Gruetter 2020-04-13 15:26:11 -0400
  • b632c66f85 More revision before class Adam Chlipala 2020-04-13 09:27:45 -0400
  • 1cc82281bf typo Samuel Gruetter 2020-04-12 21:36:38 -0400
  • 8a554ded4c Revising SeparationLogic before class Adam Chlipala 2020-04-11 14:33:14 -0400
  • 000c22f7f1 Merge branch 'master' of github.com:achlipala/frap Adam Chlipala 2020-04-08 10:48:27 -0400
  • ca3a490119 Revising before class Adam Chlipala 2020-04-08 10:48:14 -0400
  • da53b28584 HoareLogic_template: hint databases Adam Chlipala 2020-04-06 14:25:19 -0400
  • 583605fded Merge branch 'master' of github.com:achlipala/frap Adam Chlipala 2020-04-05 09:30:12 -0400
  • 477788abaa Missed loop invariant in big-step semantics Adam Chlipala 2020-04-05 09:30:01 -0400
  • 75c04e1448
         Merge pull request #40 from samuelgruetter/hoare_triple_big_step_while Adam Chlipala 2020-04-02 08:19:54 -0400
  • 1c97e1a389 explain hoare_triple_big_step_while Samuel Gruetter 2020-04-01 21:49:00 -0400
  • 7bc0425ccf
         Merge pull request #39 from bkushigian/patch-1 Adam Chlipala 2020-03-29 10:20:51 -0400
  • 01ad154c5a
         Fixed markdown inline Ben A Kushigian 2020-03-28 15:07:21 -0700
  • b5e1ae0c29 Clarify what linear_arithmetic does these days Adam Chlipala 2020-03-17 15:50:19 -0400
  • 72c0bc3a04
         Merge pull request #38 from mdempsky/parity-subtract Adam Chlipala 2020-03-17 11:24:57 -0400
  • c502399de4 Separate out library code with its own license Adam Chlipala 2020-03-17 09:22:06 -0400
  • ebcd23ee6c Add missing "O - O = E" abstraction case Matthew Dempsky 2020-03-16 12:58:20 -0700
  • 51a7fae33e Unnecessary Fixpoint Adam Chlipala 2020-03-11 09:40:55 -0400
  • dd266f2d8c Proofreading and Coq-version-updating AbstractInterpretation Adam Chlipala 2020-03-07 15:32:50 -0500
  • 64fe989cdb Turn off some warnings Adam Chlipala 2020-03-04 11:51:34 -0500
  • 19d915fb37
         Merge pull request #36 from samuelgruetter/ltac_lecture_comment Adam Chlipala 2020-03-02 11:45:36 -0500
  • 74e2399343 explain why recursive [inster] can fail Samuel Gruetter 2020-03-01 22:30:35 -0500
  • 096b69a3e9 Update LogicProgramming for Coq 8.10 Adam Chlipala 2020-03-01 10:39:01 -0500
  • d6e8cebdc9 Revising OperationalSemantics Adam Chlipala 2020-02-29 16:10:37 -0500
  • 7295e5ec60 Add TransitionSystems.vo to 'lib' target Michael137 2020-02-26 21:17:28 -0500
  • 254e2aedc6 Tiny copy-editing Adam Chlipala 2020-02-23 16:20:39 -0500
  • c2f56e1b5f Merge branch 'master' of github.com:achlipala/frap Adam Chlipala 2020-02-23 14:58:58 -0500
  • 49af9ea6a9
         Merge pull request #34 from samuelgruetter/ltac_lecture Adam Chlipala 2020-02-23 14:58:38 -0500
  • d49ca3afa8 typo Samuel Gruetter 2020-02-19 17:27:11 -0500
  • f5ca4613d7 preparing Ltac lecture Samuel Gruetter 2020-02-17 23:55:43 -0500
  • aace3dfb02 Changes based on feedback from Christopher McNally (mcncm, in #33) Adam Chlipala 2020-02-16 11:09:31 -0500
  • 728a8255f8 A little more text for the new FirstClassFunctions examples Adam Chlipala 2020-02-15 12:32:36 -0500
  • 4471c0e878 Semiring issue and two smaller fixes. mcncm 2020-02-15 11:19:35 -0500
  • af19eb9f42 Update FirstClassFunctions_template from new source material Adam Chlipala 2020-02-12 14:03:15 -0500
  • 6f17daa2df FirstClassFunctions compiles again Adam Chlipala 2020-02-12 13:53:55 -0500
  • fbf211bad2 Merge branch 'master' of github.com:achlipala/frap Adam Chlipala 2020-02-12 08:01:22 -0500
  • 6ea006fccf Truly building with Coq 8.9 again Adam Chlipala 2020-02-10 13:53:26 -0500
  • 77f22213d8 Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working Adam Chlipala 2020-02-10 13:44:35 -0500
  • c863b12c5b FirstClassFunctions: combinators for tree traversals, applied to the Interpreters imperative language Adam Chlipala 2020-02-09 16:44:22 -0500
  • fb3c957cd8 FirstClassFunctions: facts about how operations don't grow sizes Adam Chlipala 2020-02-09 15:56:25 -0500
  • 0eea46080f FirstClassFunctions: start of a new example with a language of functions over dynamically typed values Adam Chlipala 2020-02-09 14:52:00 -0500
  • 56af55f38a Revising Interpreters before class Adam Chlipala 2020-02-09 14:50:46 -0500
  • c050ec21ae Proofreading FirstClassFunctions Adam Chlipala 2020-02-09 13:17:48 -0500
  • a0993b537d Revising Interpreters before class Adam Chlipala 2020-02-09 12:54:33 -0500
  • 5e0e034263 Bump required Coq version Adam Chlipala 2020-02-09 12:26:32 -0500
  • f049d7e824 Scope fix for new N support Adam Chlipala 2020-02-08 15:18:00 -0500
  • c611524a96 Prevent more warnings for Coq 8.10 Adam Chlipala 2020-02-08 15:15:38 -0500
  • 0ed668481d Some N-related library content contributed by Sam Gruetter Adam Chlipala 2020-02-08 14:56:10 -0500
  • 89863fd999 Make 'cases' tactic handle disjunction Adam Chlipala 2020-02-08 14:47:19 -0500
  • 5a28d4fe6a Replace omega with lia Adam Chlipala 2020-02-08 14:41:07 -0500
  • d41373e0cb Link to Spring 2020 users of the book Adam Chlipala 2020-02-08 10:46:47 -0500
  • 295e095e98 Polymorphism: 8.10 update Adam Chlipala 2020-02-04 17:46:37 -0500
  • 6b737b4b0f
         Declare Scope is new as of 8.10 Andres Erbsen 2020-02-03 16:48:51 -0500
  • 290957d925 replace omega with lia Andres Erbsen 2020-02-03 14:33:06 -0500
  • 152b90e9ef Merge Adam Chlipala 2020-02-02 17:19:40 -0500
  • 89f21b8533 First phase of update for Coq 8.10 Adam Chlipala 2020-02-02 17:16:19 -0500
  • 958906a2e5 Clarify Cartesian-product operator Adam Chlipala 2020-01-08 14:36:27 -0500
  • 1fc9a126b6
         Fix typo: Abstract Syntax: '+' in Plus, not \times Dmitry Petukhov 2020-01-03 03:33:22 +0500
  • 93ef5add7a Closes #28 Adam Chlipala 2019-03-04 11:28:37 -0500
  • ed64e05e38 Closes #27 Adam Chlipala 2019-03-04 11:26:06 -0500
  • e032ab4240 Update for Coq 8.9 Adam Chlipala 2019-03-04 11:23:01 -0500
  • e92a697e33 Link to CSE 505 at UW Adam Chlipala 2018-10-27 08:22:04 -0400
  • 79e5f916b5
         Merge pull request #26 from bmsherman/book_typo Adam Chlipala 2018-05-29 14:45:32 -0400
  • 6e1e2b7ab1 Fix typo in book with label for Embeddings chapter Ben Sherman 2018-05-25 10:44:08 -0400
  • 970580d6f9 SessionTypes: LaTeX finished Adam Chlipala 2018-05-15 15:27:57 -0400
  • 7ca4318d66 SessionTypes: almost done with LaTeX chapter Adam Chlipala 2018-05-14 18:09:22 -0400
  • e7dac822fb SessionTypes: independent deadlock freedom Adam Chlipala 2018-05-13 20:06:07 -0400
  • 4874184ac9 SessionTypes: commented Adam Chlipala 2018-05-13 19:35:14 -0400
  • d839cccbad SessionTypes: starting with a more basic version Adam Chlipala 2018-05-13 18:57:53 -0400
  • 1fdf19f4f0 SessionTypes: a fuller multiparty example Adam Chlipala 2018-05-13 18:38:58 -0400
  • a86ecf84ad SessionTypes: multiparty Adam Chlipala 2018-05-13 16:52:49 -0400
  • 7fc57d795c SessionTypes: switched to modular structure, to define several variants Adam Chlipala 2018-05-13 10:32:59 -0400
  • 9f247b8375 SessionTypes: example of an online store Adam Chlipala 2018-05-13 10:27:15 -0400
  • af4a09c047 SessionTypes: changed to make choices explicitly dependent on message contents Adam Chlipala 2018-05-13 10:16:42 -0400
  • 0875f52b12 SessionTypes: deadlock freedom Adam Chlipala 2018-05-13 10:03:47 -0400
  • b9893a0e92 SessionTypes: simplified and proved a key invariant Adam Chlipala 2018-05-13 09:32:31 -0400
  • 91fc06122d Start of SessionTypes Adam Chlipala 2018-05-12 14:53:37 -0400
  • b3705cc79e Proofreading MessagesAndRefinement Adam Chlipala 2018-05-12 13:29:13 -0400
  • 0f73a3901c Proofreading ConcurrentSeparationLogic Adam Chlipala 2018-05-08 09:13:06 -0400
  • 7e84adc6bd ProgramDerivation_template Adam Chlipala 2018-05-06 19:49:10 -0400
  • d66c95a54e ProgramDerivation book chapter Adam Chlipala 2018-05-06 14:20:32 -0400
  • a8239e7925 Commented ProgramDerivation, with chapter renumbering in Coq code Adam Chlipala 2018-05-06 12:53:49 -0400