Adam Chlipala
|
254e2aedc6
|
Tiny copy-editing
|
2020-02-23 16:20:39 -05:00 |
|
Adam Chlipala
|
c2f56e1b5f
|
Merge branch 'master' of github.com:achlipala/frap
|
2020-02-23 14:58:58 -05:00 |
|
Adam Chlipala
|
49af9ea6a9
|
Merge pull request #34 from samuelgruetter/ltac_lecture
preparing Ltac lecture
|
2020-02-23 14:58:38 -05:00 |
|
Samuel Gruetter
|
d49ca3afa8
|
typo
|
2020-02-19 17:27:11 -05:00 |
|
Samuel Gruetter
|
f5ca4613d7
|
preparing Ltac lecture
|
2020-02-17 23:55:43 -05:00 |
|
Adam Chlipala
|
aace3dfb02
|
Changes based on feedback from Christopher McNally (mcncm, in #33)
|
2020-02-16 11:09:31 -05:00 |
|
Adam Chlipala
|
728a8255f8
|
A little more text for the new FirstClassFunctions examples
|
2020-02-15 12:32:36 -05:00 |
|
Adam Chlipala
|
af19eb9f42
|
Update FirstClassFunctions_template from new source material
|
2020-02-12 14:03:15 -05:00 |
|
Adam Chlipala
|
6f17daa2df
|
FirstClassFunctions compiles again
|
2020-02-12 13:53:55 -05:00 |
|
Adam Chlipala
|
fbf211bad2
|
Merge branch 'master' of github.com:achlipala/frap
|
2020-02-12 08:01:22 -05:00 |
|
Adam Chlipala
|
6ea006fccf
|
Truly building with Coq 8.9 again
|
2020-02-10 13:53:26 -05:00 |
|
Adam Chlipala
|
77f22213d8
|
Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working
|
2020-02-10 13:44:35 -05:00 |
|
Adam Chlipala
|
c863b12c5b
|
FirstClassFunctions: combinators for tree traversals, applied to the Interpreters imperative language
|
2020-02-09 16:44:22 -05:00 |
|
Adam Chlipala
|
fb3c957cd8
|
FirstClassFunctions: facts about how operations don't grow sizes
|
2020-02-09 15:56:25 -05:00 |
|
Adam Chlipala
|
0eea46080f
|
FirstClassFunctions: start of a new example with a language of functions over dynamically typed values
|
2020-02-09 14:52:00 -05:00 |
|
Adam Chlipala
|
56af55f38a
|
Revising Interpreters before class
|
2020-02-09 14:50:46 -05:00 |
|
Adam Chlipala
|
c050ec21ae
|
Proofreading FirstClassFunctions
|
2020-02-09 13:17:48 -05:00 |
|
Adam Chlipala
|
a0993b537d
|
Revising Interpreters before class
|
2020-02-09 12:54:33 -05:00 |
|
Adam Chlipala
|
5e0e034263
|
Bump required Coq version
|
2020-02-09 12:26:32 -05:00 |
|
Adam Chlipala
|
f049d7e824
|
Scope fix for new N support
|
2020-02-08 15:18:00 -05:00 |
|
Adam Chlipala
|
c611524a96
|
Prevent more warnings for Coq 8.10
|
2020-02-08 15:15:38 -05:00 |
|
Adam Chlipala
|
0ed668481d
|
Some N-related library content contributed by Sam Gruetter
|
2020-02-08 14:56:10 -05:00 |
|
Adam Chlipala
|
89863fd999
|
Make 'cases' tactic handle disjunction
|
2020-02-08 14:47:19 -05:00 |
|
Adam Chlipala
|
5a28d4fe6a
|
Replace omega with lia
|
2020-02-08 14:41:07 -05:00 |
|
Adam Chlipala
|
d41373e0cb
|
Link to Spring 2020 users of the book
|
2020-02-08 10:46:47 -05:00 |
|
Adam Chlipala
|
295e095e98
|
Polymorphism: 8.10 update
|
2020-02-04 17:46:37 -05:00 |
|
Adam Chlipala
|
152b90e9ef
|
Merge
|
2020-02-02 17:19:40 -05:00 |
|
Adam Chlipala
|
89f21b8533
|
First phase of update for Coq 8.10
|
2020-02-02 17:16:19 -05:00 |
|
Adam Chlipala
|
958906a2e5
|
Clarify Cartesian-product operator
|
2020-01-08 14:36:27 -05:00 |
|
Adam Chlipala
|
93ef5add7a
|
Closes #28
|
2019-03-04 11:28:37 -05:00 |
|
Adam Chlipala
|
ed64e05e38
|
Closes #27
|
2019-03-04 11:26:06 -05:00 |
|
Adam Chlipala
|
e032ab4240
|
Update for Coq 8.9
|
2019-03-04 11:23:01 -05:00 |
|
Adam Chlipala
|
e92a697e33
|
Link to CSE 505 at UW
|
2018-10-27 08:22:04 -04:00 |
|
Adam Chlipala
|
79e5f916b5
|
Merge pull request #26 from bmsherman/book_typo
Fix typo in book with label for Embeddings chapter
|
2018-05-29 14:45:32 -04:00 |
|
Ben Sherman
|
6e1e2b7ab1
|
Fix typo in book with label for Embeddings chapter
|
2018-05-25 10:44:08 -04:00 |
|
Adam Chlipala
|
970580d6f9
|
SessionTypes: LaTeX finished
|
2018-05-15 15:27:57 -04:00 |
|
Adam Chlipala
|
7ca4318d66
|
SessionTypes: almost done with LaTeX chapter
|
2018-05-14 18:09:22 -04:00 |
|
Adam Chlipala
|
e7dac822fb
|
SessionTypes: independent deadlock freedom
|
2018-05-13 20:06:07 -04:00 |
|
Adam Chlipala
|
4874184ac9
|
SessionTypes: commented
|
2018-05-13 19:35:14 -04:00 |
|
Adam Chlipala
|
d839cccbad
|
SessionTypes: starting with a more basic version
|
2018-05-13 18:57:53 -04:00 |
|
Adam Chlipala
|
1fdf19f4f0
|
SessionTypes: a fuller multiparty example
|
2018-05-13 18:38:58 -04:00 |
|
Adam Chlipala
|
a86ecf84ad
|
SessionTypes: multiparty
|
2018-05-13 16:52:49 -04:00 |
|
Adam Chlipala
|
7fc57d795c
|
SessionTypes: switched to modular structure, to define several variants
|
2018-05-13 10:32:59 -04:00 |
|
Adam Chlipala
|
9f247b8375
|
SessionTypes: example of an online store
|
2018-05-13 10:27:15 -04:00 |
|
Adam Chlipala
|
af4a09c047
|
SessionTypes: changed to make choices explicitly dependent on message contents
|
2018-05-13 10:16:42 -04:00 |
|
Adam Chlipala
|
0875f52b12
|
SessionTypes: deadlock freedom
|
2018-05-13 10:03:47 -04:00 |
|
Adam Chlipala
|
b9893a0e92
|
SessionTypes: simplified and proved a key invariant
|
2018-05-13 09:32:31 -04:00 |
|
Adam Chlipala
|
91fc06122d
|
Start of SessionTypes
|
2018-05-12 14:53:37 -04:00 |
|
Adam Chlipala
|
b3705cc79e
|
Proofreading MessagesAndRefinement
|
2018-05-12 13:29:13 -04:00 |
|
Adam Chlipala
|
0f73a3901c
|
Proofreading ConcurrentSeparationLogic
|
2018-05-08 09:13:06 -04:00 |
|