Commit graph

Select branches

Hide pull requests

master

#10

#11

#12

#13

#19

#20

#21

#22

#22

#23

#25

#26

#29

#3

#3

#30

#31

#33

#34

#35

#36

#38

#39

#4

#4

#40

#42

#43

#44

#48

#50

#51

#53

#55

#56

#57

#61

#61

#8

#8

#9

#9

Mono Color

• 97239a9f28
  Merge dad4d406f6 into 55d128d988 Pietro Monticone 2024-06-24 05:49:35 +0000
• 55d128d988 Italicize a term on first use (thanks to Todd Morley for the suggestion) master Adam Chlipala 2024-06-06 07:52:32 -0400
• dad4d406f6 Update frap_book.tex Pietro Monticone 2023-09-07 13:39:29 +0200
• d9fb7fca94 Wrong tactic name in comment Adam Chlipala 2023-04-23 16:09:47 -0400
• ac0a15e9f2 Rename typing relations from hasty to has_ty Adam Chlipala 2023-03-19 11:59:34 -0400
• 04be648f88 Note required Coq version Adam Chlipala 2023-02-19 16:23:56 -0500
• 2ef93d36fc Typo fix Adam Chlipala 2023-02-19 13:42:53 -0500
• 172716c8ef Latest MIT offering finished Adam Chlipala 2022-08-21 08:59:23 -0400
• 28ff5cb550 Revising for Wednesday's lecture Adam Chlipala 2022-04-18 12:58:53 -0400
• 092e3ccc1b Revising for next Wednesday's lecture Adam Chlipala 2022-04-03 14:40:20 -0400
• 0e13a0a695 Revising for tomorrow's lecture Adam Chlipala 2022-04-03 14:02:22 -0400
• 33733a0450 Revising for this week's lectures Adam Chlipala 2022-03-27 13:40:08 -0400
• c5a69b6253 Revising for tomorrow's lecture Adam Chlipala 2022-03-13 18:10:19 -0400
• f3211734b9 A big pass to stop Coq from complaining about missing locality annotations Adam Chlipala 2022-03-07 13:48:40 -0500
• b643755628
  Merge pull request #57 from al3623/master Adam Chlipala 2022-03-07 09:05:46 -0500
• b2eafc94bf Change precedence of map includes operator according to spring 21 TODO Amanda Liu 2022-03-06 23:01:31 -0500
• 955fd59327 Revising for Wednesday's lecture Adam Chlipala 2022-03-06 14:47:05 -0500
• eb53c0d714 Revising for tomorrow's lecture Adam Chlipala 2022-03-06 14:10:06 -0500
• 52e47df705 Revising for Monday's lecture Adam Chlipala 2022-02-26 15:58:03 -0500
• e3f0ada30e Revising for Wednesday's lecture Adam Chlipala 2022-02-20 12:29:17 -0500
• ddacd030e6 Revising for Tuesday's lecture Adam Chlipala 2022-02-20 12:02:38 -0500
• 23a0972d11 Revising for Wednesday's lecture Adam Chlipala 2022-02-13 14:34:23 -0500
• 0cba7c9f61 Revising for tomorrow's lecture Adam Chlipala 2022-02-13 14:16:33 -0500
• 22118d90be Update AbstractInterpretation for newer Coq versions Adam Chlipala 2022-02-06 13:13:29 -0500
• c2260bb22b
  Merge pull request #56 from al3623/cases_on_N Adam Chlipala 2022-02-06 13:04:19 -0500
• 65b817d7ae Revising for Wednesday's lecture Adam Chlipala 2022-02-06 13:03:43 -0500
• 1bff5420e2 Update cases tactic to work on N type Amanda Liu 2022-02-06 12:47:50 -0500
• bec1b1b919 Revising for tomorrow's lecture Adam Chlipala 2022-02-06 12:35:54 -0500
• f428750fdf Change notation to remain compatible with multiple Coq versions Adam Chlipala 2022-01-31 21:02:31 -0500
• 0f72c50df0 Revising for next next lecture Adam Chlipala 2022-01-29 17:22:33 -0500
• 6c1d09bbbc Revising for next lecture Adam Chlipala 2022-01-29 16:28:31 -0500
• d745f0802e Ported to Coq 8.15 Adam Chlipala 2022-01-29 15:13:09 -0500
• 1b43aa9aea Typo in function definition Adam Chlipala 2021-07-02 12:58:22 -0400
• 3582bd1222 Typo in operational semantics Adam Chlipala 2021-05-30 16:09:34 -0400
• 6986124c34 Update code index with this semester's chapter additions Adam Chlipala 2021-05-19 17:01:51 -0400
• 35d15a765d Revising for the final week of class Adam Chlipala 2021-05-16 11:55:01 -0400
• 8fdc4e2cfd Revising before this week's lectures Adam Chlipala 2021-05-10 10:45:34 -0400
• 45fa64d69e Revising for this week's lectures Adam Chlipala 2021-05-02 12:56:47 -0400
• 7e4068d5db Revising for Wednesday's lecture Adam Chlipala 2021-04-24 15:55:15 -0400
• 513e01bd3b Revising before next lecture Adam Chlipala 2021-04-24 12:59:10 -0400
• b549b15af7 Revising for next lecture Adam Chlipala 2021-04-18 16:23:25 -0400
• 796fc8d64c Noticed one invariant in HoareLogic was more complex than required Adam Chlipala 2021-04-12 16:03:38 -0400
• 1d93f6f994
  Merge pull request #55 from cpitclaudel/hoare_tweaks Adam Chlipala 2021-04-12 16:01:44 -0400
• 1e81721268 Make the ht1 tactic a bit more robust in HoareLogic.v Clément Pit-Claudel 2021-04-12 15:07:34 -0400
• 2ed1d52171 Get rid of the “reset” scope in HoareLogic.v Clément Pit-Claudel 2021-04-12 15:04:56 -0400
• 899b3dee24 Revising for this week's lectures Adam Chlipala 2021-04-11 13:32:38 -0400
• 45124f3686 Revising for Wednesday's lecture Adam Chlipala 2021-04-04 14:51:02 -0400
• d177e9fb6f Revising for tomorrow's lecture Adam Chlipala 2021-04-04 14:28:23 -0400
• 1664ddb531 EvaluationContexts_template Adam Chlipala 2021-03-30 16:12:37 -0400
• ffde22e9c9 Typo fix Adam Chlipala 2021-03-29 09:35:17 -0400
• 1c69525dc5 Typo fix Adam Chlipala 2021-03-29 09:28:33 -0400
• 75ea3ed0b3 Chapter renumbering Adam Chlipala 2021-03-28 17:03:56 -0400
• aaac5fc953 EvaluationContexts: proofreading Adam Chlipala 2021-03-28 16:59:59 -0400
• 5f1acd64e2 EvaluationContexts: finished first draft of text Adam Chlipala 2021-03-28 16:47:21 -0400
• fe1b0b2c6c EvaluationContexts: start adapting book, through products and sums Adam Chlipala 2021-03-28 16:03:42 -0400
• 6866ca2f77 EvaluationContexts: exceptions Adam Chlipala 2021-03-28 15:33:23 -0400
• 544e7fa500 EvaluationContexts: factored step0 into step0 and step1 Adam Chlipala 2021-03-28 15:12:19 -0400
• 415aa99b88 EvaluationContexts: concurrency Adam Chlipala 2021-03-28 14:58:23 -0400
• 95a28b26f6 EvaluationContexts: mutable variables Adam Chlipala 2021-03-28 14:51:12 -0400
• af135d6853 EvaluationContexts: products and sums Adam Chlipala 2021-03-28 13:28:34 -0400
• 8d1cecf7f7 EvaluationContexts: determinism Adam Chlipala 2021-03-27 20:26:37 -0400
• bcbb2181be LambdaCalculusAndTypeSoundness_template update Adam Chlipala 2021-03-27 19:15:05 -0400
• 8c2c0f5cfa LambdaCalculusAndTypeSoundness: adjust corresponding book text Adam Chlipala 2021-03-27 19:10:30 -0400
• f5aed26c77 LambdaCalculusAndTypeSoundness: remove the other use of evaluation contexts Adam Chlipala 2021-03-27 18:57:03 -0400
• 008c45351a Simplified type-soundness proof, based on an idea by Maya Sankar last year Adam Chlipala 2021-03-27 17:15:22 -0400
• 5cdd4d1322 Start of splitting evaluation contexts out of LambdaCalculusAndTypeSoundness Adam Chlipala 2021-03-27 17:03:26 -0400
• 26c272f53f Typographical fix Adam Chlipala 2021-03-27 16:17:19 -0400
• 25441b3991 Revising before class Adam Chlipala 2021-03-21 10:14:31 -0400
• 3048b59f34 Revising before tomorrow's lecture Adam Chlipala 2021-03-16 18:23:24 -0400
• d86e3278c3
  Merge pull request #53 from cpitclaudel/patch-1 Adam Chlipala 2021-03-16 15:49:30 -0400
• 4cf22df58a
  Change "there exists valuation" to "there exists a valuation" Clément Pit-Claudel 2021-03-15 19:00:41 +0000
• 3c419e5072 Revising for next lecture Adam Chlipala 2021-03-07 14:21:30 -0500
• bc9ab2a9bc Revising for today's lecture Adam Chlipala 2021-03-03 14:26:51 -0500
• 78e792e83d Fix typos Adam Chlipala 2021-03-01 17:55:28 -0500
• 4fdc85ae5c More space in template Adam Chlipala 2021-03-01 14:28:33 -0500
• d3c7a85b49 More cleanup around addition of RuleInduction Adam Chlipala 2021-03-01 12:15:34 -0500
• 890d7610d7 End of RuleInduction book chapter Adam Chlipala 2021-02-28 21:05:05 -0500
• f1bd394375 Start of RuleInduction book chapter, up through permutations Adam Chlipala 2021-02-28 18:07:31 -0500
• a55a98b426 RuleInduction: some propositional logic, with slightly naughty use of excluded middle Adam Chlipala 2021-02-28 17:19:06 -0500
• 7a906b1a63 Nicer proof of Permutation_app Adam Chlipala 2021-02-28 11:02:46 -0500
• cf7d27417d Start code for new RuleInduction chapter, up through permutation Adam Chlipala 2021-02-28 10:59:13 -0500
• 757999b52d Merge Adam Chlipala 2021-02-28 10:21:53 -0500
• b45b511969 New semester Adam Chlipala 2021-02-17 08:47:42 -0500
• d3be001671 Update before lecturing on BasicSyntax Adam Chlipala 2021-02-15 16:58:40 -0500
• d1d44e55f6 Small patch for Coq 8.13 Adam Chlipala 2021-02-14 17:26:21 -0500
• 03ffcc3e67 New semester at MIT Adam Chlipala 2021-02-14 13:04:09 -0500
• f73e30817b ConcurrentSeparationLogic_template: extend to match last change Adam Chlipala 2021-01-03 15:27:46 -0500
• b7f248e099 ConcurrentSeparationLogic: stop bothering to choose postconditions for parallel compositions, which can't terminate (addresses #52) Adam Chlipala 2021-01-03 15:20:26 -0500
• 5376847d16 Merge branch 'master' of github.com:achlipala/frap Adam Chlipala 2021-01-03 14:56:48 -0500
• f14d064555 Update for Coq 8.12.2 Adam Chlipala 2021-01-03 14:56:39 -0500
• a4cc213b75
  Merge pull request #42 from samuelgruetter/messages_typo Adam Chlipala 2021-01-03 14:41:11 -0500
• 845c9189c1
  Merge pull request #51 from mdempsky/csl-example-typo Adam Chlipala 2021-01-03 14:39:16 -0500
• 7db4d122d4
  Merge pull request #50 from mdempsky/loop-typo Adam Chlipala 2021-01-03 14:38:45 -0500
• 509ebb1d06 Fix typo in ConcurrentSeparationLogic.v example Matthew Dempsky 2020-09-24 13:30:58 -0700
• bd92c1cbb3 Fix typos in operational semantics for "Loop" command Matthew Dempsky 2020-09-24 11:43:41 -0700
• e32105c142
  Merge pull request #48 from mdempsky/sepcancel-typo Adam Chlipala 2020-07-25 09:18:19 -0400
• 0a55c03aa0 Add missing parentheses in SepCancel's normalize2 tactic Matthew Dempsky 2020-07-24 18:23:44 -0700
• d1ace360eb Parenthetical remarks to characterize in what senses various analysis results are 'most precise' (closes #47) Adam Chlipala 2020-05-22 17:10:37 -0400
• b8d0cefa6a Consistency of notation for implication (closes #46) Adam Chlipala 2020-05-11 11:50:09 -0400
• b214d2c78a Revising before class Adam Chlipala 2020-05-10 14:10:01 -0400