pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 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