pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
537 commits 1 branch 0 tags 1.6 MiB
Commit graph

134 commits

Author SHA1 Message Date
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
Adam Chlipala
6ea006fccf Truly building with Coq 8.9 again 2020-02-10 13:53:26 -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
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
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
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
d66c95a54e ProgramDerivation book chapter 2018-05-06 14:20:32 -04:00
Adam Chlipala
5201cdf524 Connecting chapter in LaTeX 2018-05-02 14:13:26 -04:00
Adam Chlipala
b74bc4b248 Proofreading SharedMemory 2018-05-01 19:43:55 -04:00
Adam Chlipala
d5c7b9d7ce Revising HoareLogic 2018-04-17 20:15:08 -04:00
Adam Chlipala
357686800a Proofreading TypesAndMutation 2018-04-08 14:15:51 -04:00
Adam Chlipala
712aacf9de Some ModelChecking improvements 2018-03-04 19:23:36 -05:00
Adam Chlipala
e8c1980257 Working with Coq 8.5pl2 again 2017-11-18 11:45:26 -05:00