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

455 commits

This branch
This branch
All branches
Author SHA1 Message Date
Adam Chlipala
4874184ac9 SessionTypes: commented 2018-05-13 19:35:14 -04:00
Adam Chlipala
d839cccbad SessionTypes: starting with a more basic version 2018-05-13 18:57:53 -04:00
Adam Chlipala
1fdf19f4f0 SessionTypes: a fuller multiparty example 2018-05-13 18:38:58 -04:00
Adam Chlipala
a86ecf84ad SessionTypes: multiparty 2018-05-13 16:52:49 -04:00
Adam Chlipala
7fc57d795c SessionTypes: switched to modular structure, to define several variants 2018-05-13 10:32:59 -04:00
Adam Chlipala
9f247b8375 SessionTypes: example of an online store 2018-05-13 10:27:15 -04:00
Adam Chlipala
af4a09c047 SessionTypes: changed to make choices explicitly dependent on message contents 2018-05-13 10:16:42 -04:00
Adam Chlipala
0875f52b12 SessionTypes: deadlock freedom 2018-05-13 10:03:47 -04:00
Adam Chlipala
b9893a0e92 SessionTypes: simplified and proved a key invariant 2018-05-13 09:32:31 -04:00
Adam Chlipala
91fc06122d Start of SessionTypes 2018-05-12 14:53:37 -04:00
Adam Chlipala
b3705cc79e Proofreading MessagesAndRefinement 2018-05-12 13:29:13 -04:00
Adam Chlipala
0f73a3901c Proofreading ConcurrentSeparationLogic 2018-05-08 09:13:06 -04:00
Adam Chlipala
7e84adc6bd ProgramDerivation_template 2018-05-06 19:49:10 -04:00
Adam Chlipala
d66c95a54e ProgramDerivation book chapter 2018-05-06 14:20:32 -04:00
Adam Chlipala
a8239e7925 Commented ProgramDerivation, with chapter renumbering in Coq code 2018-05-06 12:53:49 -04:00
Adam Chlipala
5f981335d9 ProgramDerivation: adding caches 2018-05-05 18:51:21 -04:00
Adam Chlipala
3ff400b780 ProgramDerivation: derivation of split counter 2018-05-05 15:19:12 -04:00
Adam Chlipala
4505284871 ProgramDerivation: refine_method and refine_rep 2018-05-05 14:40:51 -04:00
Adam Chlipala
2f5635938c ProgramDerivation: ADT refinement reflexivity and transitivity 2018-05-05 14:11:37 -04:00
Adam Chlipala
4171f5c286 ProgramDerivation: ADT refinement and one general principle for it 2018-05-05 12:51:46 -04:00
Adam Chlipala
cf67854a42 ProgramDerivation: starting with example from Fiat tutorial 2018-05-05 10:35:53 -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
df4016a2c3 Proofreading SharedMemory 2018-05-01 19:59:02 -04:00
Adam Chlipala
b74bc4b248 Proofreading SharedMemory 2018-05-01 19:43:55 -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
Adam Chlipala
79db2ea024
Merge pull request #25 from bmsherman/fix_minus 
minus notation should be for subtraction, not set minus
 2018-04-26 08:17:14 -04:00
Ben Sherman
fa4d8ca8db minus notation should be for subtraction, not set minus 2018-04-25 22:28:22 -04:00
Adam Chlipala
b7fd72f309 Proofreading SeparationLogic 2018-04-22 14:32:38 -04:00
Adam Chlipala
7c06dc3541 Proofreading DeepAndShallowEmbeddings 2018-04-22 14:07:01 -04:00
Adam Chlipala
d5c7b9d7ce Revising HoareLogic 2018-04-17 20:15:08 -04:00
Adam Chlipala
26365924ef DependentInductiveTypes_template 2018-04-10 18:24:03 -04:00
Adam Chlipala
b28a21620c Proofreading DependentInductiveTypes 2018-04-08 14:48:48 -04:00
Adam Chlipala
357686800a Proofreading TypesAndMutation 2018-04-08 14:15:51 -04:00
Adam Chlipala
2cb852b29c Proofreading SubsetTypes 2018-04-03 18:32:56 -04:00
Adam Chlipala
5c5cfd9600
Merge pull request #23 from k4rtik/master 
Some typo fixes
 2018-04-01 14:29:31 -04:00
Adam Chlipala
4388ecc80e Revising LambdaCalculusAndTypeSoundness 2018-04-01 13:06:47 -04:00
Kartik Singhal
1693573314 Some typo fixes 2018-03-30 14:35:57 -05:00