583 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
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
Adam Chlipala	7e84adc6bd	ProgramDerivation_template	2018-05-06 19:49:10 -04:00
Adam Chlipala	d66c95a54e	ProgramDerivation book chapter	2018-05-06 14:20:32 -04:00
Adam Chlipala	a8239e7925	Commented ProgramDerivation, with chapter renumbering in Coq code	2018-05-06 12:53:49 -04:00
Adam Chlipala	5f981335d9	ProgramDerivation: adding caches	2018-05-05 18:51:21 -04:00
Adam Chlipala	3ff400b780	ProgramDerivation: derivation of split counter	2018-05-05 15:19:12 -04:00
Adam Chlipala	4505284871	ProgramDerivation: refine_method and refine_rep	2018-05-05 14:40:51 -04:00
Adam Chlipala	2f5635938c	ProgramDerivation: ADT refinement reflexivity and transitivity	2018-05-05 14:11:37 -04:00
Adam Chlipala	4171f5c286	ProgramDerivation: ADT refinement and one general principle for it	2018-05-05 12:51:46 -04:00
Adam Chlipala	cf67854a42	ProgramDerivation: starting with example from Fiat tutorial	2018-05-05 10:35:53 -04:00
Adam Chlipala	5201cdf524	Connecting chapter in LaTeX	2018-05-02 14:13:26 -04:00