152 commits

Author	SHA1	Message	Date
Adam Chlipala	04be648f88	Note required Coq version	2023-02-19 16:23:56 -05:00
Adam Chlipala	28ff5cb550	Revising for Wednesday's lecture	2022-04-18 12:58:53 -04:00
Adam Chlipala	0e13a0a695	Revising for tomorrow's lecture	2022-04-03 14:02:22 -04:00
Adam Chlipala	33733a0450	Revising for this week's lectures	2022-03-27 13:40:08 -04:00
Adam Chlipala	e3f0ada30e	Revising for Wednesday's lecture	2022-02-20 12:29:17 -05:00
Adam Chlipala	ddacd030e6	Revising for Tuesday's lecture	2022-02-20 12:02:38 -05:00
Adam Chlipala	0cba7c9f61	Revising for tomorrow's lecture	2022-02-13 14:16:33 -05:00
Adam Chlipala	bec1b1b919	Revising for tomorrow's lecture	2022-02-06 12:35:54 -05:00
Adam Chlipala	d745f0802e	Ported to Coq 8.15	2022-01-29 15:13:09 -05:00
Adam Chlipala	1b43aa9aea	Typo in function definition	2021-07-02 12:58:22 -04:00
Adam Chlipala	3582bd1222	Typo in operational semantics	2021-05-30 16:09:34 -04:00
Adam Chlipala	35d15a765d	Revising for the final week of class	2021-05-16 11:55:01 -04:00
Adam Chlipala	8fdc4e2cfd	Revising before this week's lectures	2021-05-10 10:45:34 -04:00
Adam Chlipala	45fa64d69e	Revising for this week's lectures	2021-05-02 12:56:47 -04:00
Adam Chlipala	7e4068d5db	Revising for Wednesday's lecture	2021-04-24 15:55:15 -04:00
Adam Chlipala	513e01bd3b	Revising before next lecture	2021-04-24 12:59:10 -04:00
Adam Chlipala	899b3dee24	Revising for this week's lectures	2021-04-11 13:32:38 -04:00
Adam Chlipala	d177e9fb6f	Revising for tomorrow's lecture	2021-04-04 14:28:23 -04:00
Adam Chlipala	ffde22e9c9	Typo fix	2021-03-29 09:35:17 -04:00
Adam Chlipala	1c69525dc5	Typo fix	2021-03-29 09:28:33 -04:00
Adam Chlipala	aaac5fc953	EvaluationContexts: proofreading	2021-03-28 16:59:59 -04:00
Adam Chlipala	5f1acd64e2	EvaluationContexts: finished first draft of text	2021-03-28 16:47:21 -04:00
Adam Chlipala	fe1b0b2c6c	EvaluationContexts: start adapting book, through products and sums	2021-03-28 16:03:42 -04:00
Adam Chlipala	8c2c0f5cfa	LambdaCalculusAndTypeSoundness: adjust corresponding book text	2021-03-27 19:10:30 -04:00
Adam Chlipala	5cdd4d1322	Start of splitting evaluation contexts out of LambdaCalculusAndTypeSoundness	2021-03-27 17:03:26 -04:00
Adam Chlipala	26c272f53f	Typographical fix	2021-03-27 16:17:19 -04:00
Adam Chlipala	25441b3991	Revising before class	2021-03-21 10:14:31 -04:00
Clément Pit-Claudel	4cf22df58a	Change "there exists valuation" to "there exists a valuation"	2021-03-15 19:00:41 +00:00
Adam Chlipala	bc9ab2a9bc	Revising for today's lecture	2021-03-03 14:26:51 -05:00
Adam Chlipala	78e792e83d	Fix typos	2021-03-01 17:55:28 -05:00
Adam Chlipala	d3c7a85b49	More cleanup around addition of RuleInduction	2021-03-01 12:15:34 -05:00
Adam Chlipala	890d7610d7	End of RuleInduction book chapter	2021-02-28 21:05:05 -05:00
Adam Chlipala	f1bd394375	Start of RuleInduction book chapter, up through permutations	2021-02-28 18:07:31 -05:00
Adam Chlipala	d3be001671	Update before lecturing on BasicSyntax	2021-02-15 16:58:40 -05:00
Adam Chlipala	b7f248e099	ConcurrentSeparationLogic: stop bothering to choose postconditions for parallel compositions, which can't terminate (addresses #52)	2021-01-03 15:20:26 -05:00
Matthew Dempsky	bd92c1cbb3	Fix typos in operational semantics for "Loop" command ... In section 13.3, the type of Loop is defined as: Loop : forall a, a -> (a -> cmd (outcome a)) -> cmd a However, the operational semantics provided in sections 14.1 and 18.1 invoke the loop body function using "Again(i)" (type "outcome a"). They should instead use simply "i" (type "a"). Changing to "f(i)" also matches the StepLoop formalizations in SeparationLogic.v and ConcurrentSeparationLogic.v, which invoke simply "body init" (rather than "body (Again init)").	2020-09-24 11:43:41 -07:00
Adam Chlipala	d1ace360eb	Parenthetical remarks to characterize in what senses various analysis results are 'most precise' (closes #47)	2020-05-22 17:10:37 -04:00
Adam Chlipala	b8d0cefa6a	Consistency of notation for implication (closes #46)	2020-05-11 11:50:09 -04:00
Adam Chlipala	8a87c209f7	Revising before class	2020-05-05 19:26:59 -04:00
Adam Chlipala	5f735225ef	Revising before class	2020-04-28 09:40:40 -04:00
Adam Chlipala	eccb504f08	Merge pull request #43 from bkushigian/master ... Change overloaded term `S` in section 5.4	2020-04-24 09:29:23 -04:00
bkushigian	22f3238a8a	Change overloaded term S in section 5.4	2020-04-20 09:34:30 -07:00
Adam Chlipala	69de20dec8	Revising before class, including with an optimization to the model-checking engine	2020-04-20 11:56:23 -04:00
Adam Chlipala	c607913898	Typo in translation rule	2020-04-15 09:48:24 -04:00
Adam Chlipala	2efec7b61d	Typo fix	2020-04-14 11:55:26 -04:00
Adam Chlipala	b632c66f85	More revision before class	2020-04-13 09:27:45 -04:00
Adam Chlipala	477788abaa	Missed loop invariant in big-step semantics	2020-04-05 09:30:01 -04:00
Adam Chlipala	b5e1ae0c29	Clarify what linear_arithmetic does these days	2020-03-17 15:50:19 -04:00
Matthew Dempsky	ebcd23ee6c	Add missing "O - O = E" abstraction case ... This case is implemented by parity_subtract in AbstractInterpretation.v and is necessary to calculate the "most precise abstraction." See also #28, #37.	2020-03-16 12:58:20 -07:00
Adam Chlipala	aace3dfb02	Changes based on feedback from Christopher McNally (mcncm, in #33)	2020-02-16 11:09:31 -05:00