Commit Graph

146 Commits

Author SHA1 Message Date
Denis Merigoux
d8b18c80b8
Fixed syntax cheat sheet for extremum 2021-07-15 14:55:32 +02:00
EmileRolley
b32f0bf0a4 docs(syntax): add the duration division operator + fix the catala_en syntax highlighting 2021-05-31 10:26:51 +02:00
Denis Merigoux
faedeaf3ce
Pull proof robustness modifications from ICFP21 artefact 2021-05-20 11:21:29 +02:00
Denis Merigoux
3c8d187be0
Big refactoring of the literate programming structure
Partially fixes #120
Removes the distinction between headers and articles, streamlines the surface AST
Changes affects lexers and parser
2021-05-15 01:16:08 +02:00
EmileRolley
a594220313 docs(images): add file icons 2021-04-06 11:56:02 +02:00
EmileRolley
188324a361 docs(images): add an alternative logo 2021-04-06 10:37:30 +02:00
Denis Merigoux
29a066684c Change date syntax 2021-03-21 19:48:04 +01:00
Denis Merigoux
ef85b06bc1
Update syntax cheat sheet 2021-03-19 19:33:38 +01:00
Denis Merigoux
88cbe1fc9f
Update screenshot 2021-03-16 19:11:31 +01:00
Denis Merigoux
7edc3aa768
Added duration literal 2021-03-15 14:57:11 +01:00
Denis Merigoux
f6c1417a95
Finished syntax cheat sheet 2021-03-15 11:12:24 +01:00
Denis Merigoux
3b110e04ee
Syntax sheet 2021-03-14 21:57:01 +01:00
EmileRolley
3910451fc8 docs: modify README.md's screenshots size 2021-03-10 15:20:44 +01:00
EmileRolley
e2d7f0c57d docs: modify README.md's screenshots width 2021-03-10 15:15:47 +01:00
EmileRolley
2d6add938d docs(images): removes the background color from the VSCode screenshot 2021-03-10 15:01:43 +01:00
EmileRolley
f0cfe034d4 docs(images): update the ScreenShotVSCode with the new syntax 2021-03-10 14:54:24 +01:00
Denis Merigoux
fdb1975865 Link to paper 2021-03-05 19:19:10 +01:00
Denis Merigoux
7d7fe7b09d Remove latex rule 2021-03-03 13:38:17 +01:00
Denis Merigoux
807f707b8a Updated README 2021-03-03 12:32:16 +01:00
Denis Merigoux
1c9d2dc696 Killed the last suspicious admit 2021-03-03 12:23:16 +01:00
Denis Merigoux
0b8e93348a Added README 2021-03-03 03:20:47 +01:00
Denis Merigoux
f342649211 Stabilized proofs 2021-03-03 03:05:58 +01:00
Denis Merigoux
5f144d3157 Proof is in an acceptable state, mission accomplished 2021-03-03 01:20:00 +01:00
Denis Merigoux
5241b0e64b Finished main big lemma proof over heavy stepping 2021-03-03 00:52:37 +01:00
Denis Merigoux
00569a8304 Some proof progress 2021-03-02 23:30:01 +01:00
Denis Merigoux
573d07428c Killed another admit 2021-03-02 20:47:44 +01:00
Denis Merigoux
4610dc2b92 One lemma proven with an administrative assume 2021-03-02 20:05:24 +01:00
Denis Merigoux
892b6daeee Most admits concern LCalc stepping + 1 assume for semantics of process_exceptions compared to empty_count 2021-02-22 01:18:05 +01:00
Denis Merigoux
ad54dfe691 Added dumb invariance lemma 2021-02-22 00:30:03 +01:00
Denis Merigoux
1071f3232d Proof went until the end, now havee to remove admits 2021-02-21 23:55:01 +01:00
Denis Merigoux
b2d9407c2b Fixed error and some mixup 2021-02-21 20:56:15 +01:00
Denis Merigoux
f14235fa5e All values case done 2021-02-21 20:23:13 +01:00
Denis Merigoux
80f2dffe1d Yet another proof case 2021-02-21 19:17:51 +01:00
Denis Merigoux
038c5b3e07 Proven one more subcase 2021-02-21 18:51:36 +01:00
Denis Merigoux
4efccbb335 Found theorem for all exceptions values 2021-02-21 17:24:52 +01:00
Denis Merigoux
6c881f7afb Code refactor 2021-02-21 16:38:52 +01:00
Denis Merigoux
ed4f589acb Proof structure of exceptions stepping case done 2021-02-21 16:15:17 +01:00
Denis Merigoux
c686b77b1d Proven case where tail steps to error 2021-02-21 15:27:33 +01:00
Denis Merigoux
8d5aa8e86e Split big theroem to manage it 2021-02-21 14:58:37 +01:00
Denis Merigoux
94b1c348d6 Weakened theorem to ensure good recursion 2021-02-21 14:38:11 +01:00
Denis Merigoux
38f7b72604 Restored proof again 2021-02-21 14:27:10 +01:00
Denis Merigoux
dbc8133821 Found correct version of exception stepping theorem 2021-02-21 13:24:27 +01:00
Denis Merigoux
68c36b26a1 Making slow progress 2021-02-21 00:36:06 +01:00
Denis Merigoux
e926adf6f0 Added thunk to ease proof of substitution correctness 2021-02-20 22:38:10 +01:00
Denis Merigoux
2efdd71866 Restored the proof somewhat 2021-02-20 20:31:51 +01:00
Denis Merigoux
b3fd1c030a proof of typing_empty_can_be_extended 2021-02-20 11:41:48 +01:00
Denis Merigoux
5b92165867 Restored type safety of lambda calculus 2021-02-19 22:06:09 +01:00
Denis Merigoux
9b4466b836 Type safety of default calculus restoed 2021-02-19 19:01:23 +01:00
Denis Merigoux
6662a07bfd Making progress on default calculus 2021-02-19 15:09:39 +01:00
Denis Merigoux
21cf048a19 Starting transition to De Bruijn 2021-02-19 14:01:27 +01:00