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

534 commits

This branch
This branch
All branches
Author SHA1 Message Date
Adam Chlipala
75ea3ed0b3 Chapter renumbering 2021-03-28 17:03:56 -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
6866ca2f77 EvaluationContexts: exceptions 2021-03-28 15:33:23 -04:00
Adam Chlipala
544e7fa500 EvaluationContexts: factored step0 into step0 and step1 2021-03-28 15:12:19 -04:00
Adam Chlipala
415aa99b88 EvaluationContexts: concurrency 2021-03-28 14:58:23 -04:00
Adam Chlipala
95a28b26f6 EvaluationContexts: mutable variables 2021-03-28 14:51:12 -04:00
Adam Chlipala
af135d6853 EvaluationContexts: products and sums 2021-03-28 13:28:34 -04:00
Adam Chlipala
8d1cecf7f7 EvaluationContexts: determinism 2021-03-27 20:26:37 -04:00
Adam Chlipala
bcbb2181be LambdaCalculusAndTypeSoundness_template update 2021-03-27 19:15:05 -04:00
Adam Chlipala
8c2c0f5cfa LambdaCalculusAndTypeSoundness: adjust corresponding book text 2021-03-27 19:10:30 -04:00
Adam Chlipala
f5aed26c77 LambdaCalculusAndTypeSoundness: remove the other use of evaluation contexts 2021-03-27 18:57:03 -04:00
Adam Chlipala
008c45351a Simplified type-soundness proof, based on an idea by Maya Sankar last year 2021-03-27 17:15:22 -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
Adam Chlipala
3048b59f34 Revising before tomorrow's lecture 2021-03-16 18:23:24 -04:00
Adam Chlipala
d86e3278c3
Merge pull request #53 from cpitclaudel/patch-1 
Change "there exists valuation" to "there exists a valuation"
 2021-03-16 15:49:30 -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
3c419e5072 Revising for next lecture 2021-03-07 14:21:30 -05: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
4fdc85ae5c More space in template 2021-03-01 14:28:33 -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
a55a98b426 RuleInduction: some propositional logic, with slightly naughty use of excluded middle 2021-02-28 17:19:06 -05:00
Adam Chlipala
7a906b1a63 Nicer proof of Permutation_app 2021-02-28 11:02:46 -05:00
Adam Chlipala
cf7d27417d Start code for new RuleInduction chapter, up through permutation 2021-02-28 10:59:13 -05:00
Adam Chlipala
757999b52d Merge 2021-02-28 10:21:53 -05:00
Adam Chlipala
b45b511969 New semester 2021-02-17 08:47:42 -05:00
Adam Chlipala
d3be001671 Update before lecturing on BasicSyntax 2021-02-15 16:58:40 -05:00
Adam Chlipala
d1d44e55f6 Small patch for Coq 8.13 2021-02-14 17:26:21 -05:00
Adam Chlipala
03ffcc3e67 New semester at MIT 2021-02-14 13:04:09 -05:00
Adam Chlipala
f73e30817b ConcurrentSeparationLogic_template: extend to match last change 2021-01-03 15:27:46 -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
Adam Chlipala
5376847d16 Merge branch 'master' of github.com:achlipala/frap 2021-01-03 14:56:48 -05:00
Adam Chlipala
f14d064555 Update for Coq 8.12.2 2021-01-03 14:56:39 -05:00
Adam Chlipala
a4cc213b75
Merge pull request #42 from samuelgruetter/messages_typo 
typo
 2021-01-03 14:41:11 -05:00
Adam Chlipala
845c9189c1
Merge pull request #51 from mdempsky/csl-example-typo 
Fix typo in ConcurrentSeparationLogic.v example
 2021-01-03 14:39:16 -05:00
Adam Chlipala
7db4d122d4
Merge pull request #50 from mdempsky/loop-typo 
Fix typos in operational semantics for "Loop" command
 2021-01-03 14:38:45 -05:00
Matthew Dempsky
509ebb1d06 Fix typo in ConcurrentSeparationLogic.v example 
In the 3-stage example, the middle stage moves list elements from the
first stack to the second stack, not back onto the first stack again.
 2020-09-24 13:30:58 -07: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
e32105c142
Merge pull request #48 from mdempsky/sepcancel-typo 
Add missing parentheses in SepCancel's normalize2 tactic
 2020-07-25 09:18:19 -04:00
Matthew Dempsky
0a55c03aa0 Add missing parentheses in SepCancel's normalize2 tactic 
Before this change, "Print normalize2" prints:

    Ltac Frap.SepCancel.Make.normalize2 :=
      match goal with
      | |- context [ (?p * lift) (?P /\ ?Q) ] => rewrite (lift_uncombine p P Q)
      | |- context [ ?p * (?q * ?r) ] => rewrite (star_assoc p q r)
      end

After, it prints:

    Ltac Frap.SepCancel.Make.normalize2 :=
      match goal with
      | |- context [ ?p * [|?P /\ ?Q|] ] => rewrite (lift_uncombine p P Q)
      | |- context [ ?p * (?q * ?r) ] => rewrite (star_assoc p q r)
      end
 2020-07-24 18:23:44 -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
b214d2c78a Revising before class 2020-05-10 14:10:01 -04:00
Adam Chlipala
8a87c209f7 Revising before class 2020-05-05 19:26:59 -04:00