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
583 commits 1 branch 0 tags 1.6 MiB
Commit graph

21 commits

Author SHA1 Message Date
Adam Chlipala
f3211734b9 A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
Adam Chlipala
d745f0802e Ported to Coq 8.15 2022-01-29 15:13:09 -05:00
Adam Chlipala
7e4068d5db Revising for Wednesday's lecture 2021-04-24 15:55:15 -04:00
Adam Chlipala
75ea3ed0b3 Chapter renumbering 2021-03-28 17:03:56 -04:00
Adam Chlipala
d3c7a85b49 More cleanup around addition of RuleInduction 2021-03-01 12:15:34 -05:00
Adam Chlipala
d74a0ebb42 Revising before class 2020-04-14 15:48:36 -04:00
Adam Chlipala
5201cdf524 Connecting chapter in LaTeX 2018-05-02 14:13:26 -04:00
Adam Chlipala
369edcdd79 Update for new Connecting chapter, modulo adding the LaTeX content 2018-05-02 11:56:01 -04:00
Adam Chlipala
8ce5c8fb0b Connecting: pretty-printing C code 2018-04-30 13:23:57 -04:00
Adam Chlipala
869b70561f Connecting: extracting list reverse 2018-04-30 12:54:04 -04:00
Adam Chlipala
09ac8af058 Connecting: admit-free again 2018-04-30 12:17:27 -04:00
Adam Chlipala
b748ee570b Connecting: only admits left are about map equality 2018-04-30 10:18:41 -04:00
Adam Chlipala
ba72a971dc Connecting: failure is not an option 2018-04-29 21:24:49 -04:00
Adam Chlipala
82db018daf Connecting: writing 2018-04-29 21:23:46 -04:00
Adam Chlipala
51a1b7c445 Connecting: ditch head and tail 2018-04-29 21:11:21 -04:00
Adam Chlipala
daebf21dc0 Connecting: reading heads 2018-04-29 21:08:12 -04:00
Adam Chlipala
d537e28266 Connecting: parameterizing translation in a way that should support loops later 2018-04-29 20:33:51 -04:00
Adam Chlipala
ca6d577f84 Connecting: added a heap relation, but at the moment it could be anything, because no heap-accessing commands are supported 2018-04-29 17:25:03 -04:00
Adam Chlipala
6b3a93a8b2 Connecting: proved an invariant for a compilation result 2018-04-29 16:57:47 -04:00
Adam Chlipala
26abb7b8a0 Connecting: proved DeeplyEmbedded.hoare_triple_sound 2018-04-28 21:23:41 -04:00
Adam Chlipala
625458d80e Connecting: proved DeeplyEmbedded.preservation 2018-04-28 20:31:01 -04:00