Commit graph

Select branches

Hide pull requests

master

#10

#11

#12

#13

#19

#20

#21

#22

#22

#23

#25

#26

#29

#3

#3

#30

#31

#33

#34

#35

#36

#38

#39

#4

#4

#40

#42

#43

#44

#48

#50

#51

#53

#55

#56

#57

#61

#61

#8

#8

#9

#9

Mono Color

• 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