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

• 5f981335d9 ProgramDerivation: adding caches Adam Chlipala 2018-05-05 18:51:21 -0400
• 3ff400b780 ProgramDerivation: derivation of split counter Adam Chlipala 2018-05-05 15:19:12 -0400
• 4505284871 ProgramDerivation: refine_method and refine_rep Adam Chlipala 2018-05-05 14:40:51 -0400
• 2f5635938c ProgramDerivation: ADT refinement reflexivity and transitivity Adam Chlipala 2018-05-05 14:11:37 -0400
• 4171f5c286 ProgramDerivation: ADT refinement and one general principle for it Adam Chlipala 2018-05-05 12:51:46 -0400
• cf67854a42 ProgramDerivation: starting with example from Fiat tutorial Adam Chlipala 2018-05-05 10:35:53 -0400
• 5201cdf524 Connecting chapter in LaTeX Adam Chlipala 2018-05-02 14:13:26 -0400
• 369edcdd79 Update for new Connecting chapter, modulo adding the LaTeX content Adam Chlipala 2018-05-02 11:56:01 -0400
• df4016a2c3 Proofreading SharedMemory Adam Chlipala 2018-05-01 19:59:02 -0400
• b74bc4b248 Proofreading SharedMemory Adam Chlipala 2018-05-01 19:43:55 -0400
• 8ce5c8fb0b Connecting: pretty-printing C code Adam Chlipala 2018-04-30 13:23:57 -0400
• 869b70561f Connecting: extracting list reverse Adam Chlipala 2018-04-30 12:54:04 -0400
• 09ac8af058 Connecting: admit-free again Adam Chlipala 2018-04-30 12:17:27 -0400
• b748ee570b Connecting: only admits left are about map equality Adam Chlipala 2018-04-30 10:18:41 -0400
• ba72a971dc Connecting: failure is not an option Adam Chlipala 2018-04-29 21:24:49 -0400
• 82db018daf Connecting: writing Adam Chlipala 2018-04-29 21:23:46 -0400
• 51a1b7c445 Connecting: ditch head and tail Adam Chlipala 2018-04-29 21:11:21 -0400
• daebf21dc0 Connecting: reading heads Adam Chlipala 2018-04-29 21:08:12 -0400
• d537e28266 Connecting: parameterizing translation in a way that should support loops later Adam Chlipala 2018-04-29 20:33:51 -0400
• ca6d577f84 Connecting: added a heap relation, but at the moment it could be anything, because no heap-accessing commands are supported Adam Chlipala 2018-04-29 17:25:03 -0400
• 6b3a93a8b2 Connecting: proved an invariant for a compilation result Adam Chlipala 2018-04-29 16:57:47 -0400
• 26abb7b8a0 Connecting: proved DeeplyEmbedded.hoare_triple_sound Adam Chlipala 2018-04-28 21:23:41 -0400
• 625458d80e Connecting: proved DeeplyEmbedded.preservation Adam Chlipala 2018-04-28 20:31:01 -0400
• 79db2ea024
  Merge pull request #25 from bmsherman/fix_minus Adam Chlipala 2018-04-26 08:17:14 -0400
• fa4d8ca8db minus notation should be for subtraction, not set minus Ben Sherman 2018-04-25 22:28:22 -0400
• b7fd72f309 Proofreading SeparationLogic Adam Chlipala 2018-04-22 14:32:38 -0400
• 7c06dc3541 Proofreading DeepAndShallowEmbeddings Adam Chlipala 2018-04-22 14:07:01 -0400
• d5c7b9d7ce Revising HoareLogic Adam Chlipala 2018-04-17 20:15:08 -0400
• 26365924ef DependentInductiveTypes_template Adam Chlipala 2018-04-10 18:24:03 -0400
• b28a21620c Proofreading DependentInductiveTypes Adam Chlipala 2018-04-08 14:48:48 -0400
• 357686800a Proofreading TypesAndMutation Adam Chlipala 2018-04-08 14:15:51 -0400
• 2cb852b29c Proofreading SubsetTypes Adam Chlipala 2018-04-03 18:32:56 -0400
• 5c5cfd9600
  Merge pull request #23 from k4rtik/master Adam Chlipala 2018-04-01 14:29:31 -0400
• 4388ecc80e Revising LambdaCalculusAndTypeSoundness Adam Chlipala 2018-04-01 13:06:47 -0400
• 1693573314 Some typo fixes Kartik Singhal 2018-03-30 14:35:57 -0500
• 2269b38367 Proofreading CompilerCorrectness Adam Chlipala 2018-03-21 07:14:12 -0400
• 4bf1c3fc7c Increase precision of abstract subtraction for parity (thanks to Aleksejs Popovs for the suggestion) Adam Chlipala 2018-03-20 17:18:31 -0400
• f46bed19bb Proofreading AbstractInterpretation Adam Chlipala 2018-03-18 20:45:46 -0400
• a48d85c84c Improve robustness of set simplification Adam Chlipala 2018-03-17 19:35:43 -0400
• c8cfde5acf Proofreading LogicProgramming Adam Chlipala 2018-03-13 20:26:17 -0400
• 02a0959e4a
  Merge 47d82f10b8 into 078e29f8a9 Lef Ioannidis 2018-03-10 21:25:37 +0000
• 47d82f10b8
  Update frap_book.tex Lef Ioannidis 2018-03-10 16:23:58 -0500
• 078e29f8a9 ProofByReflection: some copyediting Adam Chlipala 2018-03-06 20:29:57 -0500
• 712aacf9de Some ModelChecking improvements Adam Chlipala 2018-03-04 19:23:36 -0500
• b0ad93e6a4 Fix up ModelChecking to track a change in TransitionSystems Adam Chlipala 2018-03-04 18:46:12 -0500
• a501f5e1ec
  Merge pull request #21 from bmsherman/master Adam Chlipala 2018-03-02 11:36:33 -0500
• 76970fb98e Small improvements to IntroToProofScripting Adam Chlipala 2018-02-28 09:01:07 -0500
• 256995f1dd Typo fixes Adam Chlipala 2018-02-25 19:40:10 -0500
• 1d105aef0e TransitionSystems: give more meaningful names to parallel trsys components Ben Sherman 2018-02-21 16:45:15 -0500
• 49b23293ca FirstClassFunctions_template Adam Chlipala 2018-02-19 21:00:21 -0500
• c192b2d7cb FirstClassFunctions: comments Adam Chlipala 2018-02-19 20:39:07 -0500
• 5de80d6d53 FirstClassFunctions: insertion sort Adam Chlipala 2018-02-19 14:47:40 -0500
• 399e8f7228 FirstClassFunctions: move bruisingly long proof to end Adam Chlipala 2018-02-19 14:13:57 -0500
• 63836dad24 FirstClassFunctions: flattenS_ok Adam Chlipala 2018-02-19 14:02:17 -0500
• 0047d49139 FirstClassFunctions: flattenKD_ok Adam Chlipala 2018-02-18 20:15:10 -0500
• 3e689a9a4a FirstClassFunctions: fix later examples Adam Chlipala 2018-02-18 18:19:39 -0500
• 5019b2561e FirstClassFunctions: big old scary proof of sublistSummingToK_ok Adam Chlipala 2018-02-18 16:46:12 -0500
• a30079d6b4 FirstClassFunctions: CPS versions of classics Adam Chlipala 2018-02-18 13:05:56 -0500
• 3a018fbf16 Start of FirstClassFunctions Adam Chlipala 2018-02-18 12:49:36 -0500
• 54576fa373 Revising Polymorphism Adam Chlipala 2018-02-11 19:06:52 -0500
• 49a020a348 6.822 Spring 2018 Adam Chlipala 2017-12-18 17:08:23 -0500
• c6cc13587c Working again with Coq 8.6.1 Adam Chlipala 2017-11-18 12:15:15 -0500
• e8c1980257 Working with Coq 8.5pl2 again Adam Chlipala 2017-11-18 11:45:26 -0500
• 1ee699431c Change ProofByReflection to work in Coq 8.6.1 Adam Chlipala 2017-11-18 10:43:08 -0500
• 19e9e84953 Merge pull request #20 from andres-erbsen/patch-1 Adam Chlipala 2017-09-10 14:05:46 -0400
• 2f8adc23a9 11.1: s/smallstep/smallstepo/ to match Coq source Andres Erbsen 2017-09-06 12:06:34 -0400
• 103c8ad557 Add web links to exercises Adam Chlipala 2017-06-03 12:54:51 -0400
• f25ef97f8f Merge 40abba73e5 into 1bd9880e62 jankcorn 2017-05-22 12:05:38 +0000
• 1bd9880e62 Typo fix Adam Chlipala 2017-05-14 15:58:04 -0400
• e4442e6e29 SharedMemory: don't need exponentiation after all Adam Chlipala 2017-05-14 15:43:21 -0400
• 6e76010a86 CompilerCorrectness: explain why we need so many kinds of simulations Adam Chlipala 2017-05-14 15:23:57 -0400
• 1721d678af Backward reference from MessagesAndRefinement to CompilerCorrectness Adam Chlipala 2017-05-14 15:11:34 -0400
• 9550a02a37 Make [sets] tactic more robust to type synonyms Adam Chlipala 2017-05-14 12:50:18 -0400
• 962936a80d Merge pull request #19 from k4rtik/patch-1 Adam Chlipala 2017-05-12 14:04:48 -0400
• c9a02eeecb Fix typo Kartik Singhal 2017-05-05 21:32:14 -0400
• 44a56e7259 SharedMemory: update book text Adam Chlipala 2017-04-30 22:05:28 -0400
• f8752d9b1c SharedMemory: finished new simpler Coq proof (with restricted applicability) Adam Chlipala 2017-04-30 21:26:05 -0400
• 824d4bc524 Checkpoint simplifying SharedMemory Adam Chlipala 2017-04-30 20:05:19 -0400
• db0f87d654 DeepAndShallowEmbeddings: comment typo fix Adam Chlipala 2017-04-24 09:28:48 -0400
• a6624bdcf2 Typo fix in book Adam Chlipala 2017-04-18 21:01:12 -0400
• 9928399f5c Small typo fix in Chapter 11 Adam Chlipala 2017-04-09 09:40:31 -0400
• d8e580b331 DependentInductiveTypes Adam Chlipala 2017-04-02 20:50:10 -0400
• e204041ff8 Tiny revisions to LambdaCalculusAndTypeSoundness Adam Chlipala 2017-04-02 19:18:34 -0400
• 119996a90c SubsetTypes_template Adam Chlipala 2017-03-22 09:15:33 -0400
• 31b0b6e9e5 SubsetTypes_template Adam Chlipala 2017-03-22 09:15:22 -0400
• e9e8e6b92b Add two library lemmas Adam Chlipala 2017-03-21 21:39:37 -0400
• c5600db874 SubsetTypes Adam Chlipala 2017-03-21 19:27:36 -0400
• 88df5601f5 CompilerCorrectness_template Adam Chlipala 2017-03-19 20:09:48 -0400
• 5df1caf940 CompilerCorrectness chapter: proofreading Adam Chlipala 2017-03-19 18:39:05 -0400
• cefe711466 CompilerCorrectness chapter: simulation with multiple matching steps Adam Chlipala 2017-03-19 18:21:30 -0400
• 6c1af44f95 CompilerCorrectness chapter: simulation with skipping, after adding termination as an observable Adam Chlipala 2017-03-19 18:07:21 -0400
• 9974e130f0 CompilerCorrectness chapter: basic simulation and constant folding Adam Chlipala 2017-03-19 16:36:04 -0400
• 882c6868ec Start of CompilerCorrectness chapter: trace equivalence Adam Chlipala 2017-03-19 16:07:07 -0400
• b11fede54e CompilerCorrectness: comments and a medium-size simplification of flattening Adam Chlipala 2017-03-19 15:27:40 -0400
• dd7ce9f869 CompilerCorrectness: a running example program to optimize Adam Chlipala 2017-03-19 14:29:56 -0400
• 7cebd4bfba CompilerCorrectness: flatten_ok Adam Chlipala 2017-03-19 14:04:51 -0400
• c4be95afab CompilerCorrectness: simulation_multiple Adam Chlipala 2017-03-19 12:32:40 -0400
• a9ba30076d Merge Adam Chlipala 2017-03-18 20:20:23 -0400
• bf85fa5c2c CompilerCorrectness: cfold_ok, both directions Adam Chlipala 2017-03-18 17:22:12 -0400
• 829b6a4304 CompilerCorrectness: cfold_ok, in only one direction Adam Chlipala 2017-03-18 15:23:45 -0400