CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 16:28:12 +03:00
Code Issues Projects Releases Wiki Activity
3,846 Commits 40 Branches 8 Tags 60 MiB
e308ff8d02
Commit Graph

179 Commits

Author SHA1 Message Date
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
Denis Merigoux
cfd2a4bcc3 WIP 2021-02-18 16:12:23 +01:00
Denis Merigoux
c2dc8db6ac Fix list stepping semantics in both default and lambda calculus 2021-02-17 16:24:19 +01:00
Denis Merigoux
f70a4af7b4 More general theorem, second difficult case OK 2021-02-16 16:20:42 +01:00
Denis Merigoux
ddfc67af55 Prove small precedes lemma 2021-02-15 22:01:37 +01:00
Denis Merigoux
35ae5ff39a Flesh out other case; more general theorem needed 2021-02-15 20:06:33 +01:00
Denis Merigoux
7711cad2f4 First case fully proven 2021-02-15 16:18:20 +01:00
Denis Merigoux
d7cfbb2eba First case of difficult translation proven 2021-02-15 14:18:55 +01:00
Denis Merigoux
9ffb0c134e Proved one complicated lift 2021-02-15 11:35:51 +01:00
Denis Merigoux
adf16489bf Back to simpler version of step commute 2021-02-14 23:25:29 +01:00
Denis Merigoux
e3e3896d0a Some progress 2021-02-14 22:47:40 +01:00
Denis Merigoux
fe5c5d8165 Ready for push on exceptions stepping 2021-02-12 18:29:10 +01:00
Denis Merigoux
f29bdeb4ac Missing default proof but now with typing and correct lift 2021-02-12 17:06:38 +01:00
Denis Merigoux
e8ed143663 Restored sanity to proof 2021-02-12 16:01:31 +01:00
Denis Merigoux
9773c11fb2 Fixed error propagation in lists 2021-02-12 15:02:40 +01:00
Denis Merigoux
eb0b702b4d Some progress 2021-02-12 11:02:47 +01:00
Denis Merigoux
dff14e67ca More proof progress 2021-02-11 18:49:40 +01:00
Denis Merigoux
cf88f12cdb Some work on the theorem 2021-02-10 19:29:43 +01:00
Denis Merigoux
d0e5e32854 Last case very difficult 2021-02-09 12:49:52 +01:00
Denis Merigoux
7ed0477303 Missing only last little case 2021-02-08 20:11:46 +01:00
Denis Merigoux
ec03ad8892 Fixed list semantics to prove first case of big theorem 2021-02-08 13:51:56 +01:00
Denis Merigoux
f3a38eeab6 Beginning to attack last trickiest theorem 2021-02-08 12:24:51 +01:00
Denis Merigoux
e68d86a3cb Fist theorem proven 2021-02-08 10:17:38 +01:00
Denis Merigoux
71f3c29b26 Added silent variables in target lambda calculus 2021-02-08 10:03:57 +01:00
Denis Merigoux
08883e04a9 Beginning to attack first certification theorem 2021-02-07 22:38:04 +01:00
Denis Merigoux
774e31245b Translation defined, proof to come 2021-02-07 19:35:00 +01:00
Denis Merigoux
014056794d Beginning to write the translatio 2021-02-07 16:10:01 +01:00
Denis Merigoux
736c49507c Robust and complete proof of type safety for the lambda calculus 2021-02-07 15:36:30 +01:00
Denis Merigoux
8875408665 Preservation proven 2021-02-06 19:05:11 +01:00
Denis Merigoux
6df17f7039 Missing preservation only for lambda calculus 2021-02-06 18:01:17 +01:00
Denis Merigoux
6a8b0b6c88 Progress proven for lambda calculus 2021-02-05 17:29:45 +01:00
Denis Merigoux
7fb5a4280b Begin formalization of target lambda calculus 2021-02-05 15:28:26 +01:00
Denis Merigoux
423e6aff10 Formalized compilation scheme and proved correctness on paper 2021-02-02 13:16:58 +01:00
Denis Merigoux
26c2458df4 Update formalization in F* 2021-01-27 19:59:00 +01:00
Denis Merigoux
430ba0d429 Finished first draft of default compilation formalization 2021-01-27 09:58:58 +01:00
Denis Merigoux
6b1c6fad5d More compilation discussion 2021-01-27 09:58:58 +01:00
Denis Merigoux
a81a50334b Beginning formalization 2021-01-27 09:58:58 +01:00
Denis Merigoux
85ef15ec09 Printing correct position information inside law 2021-01-20 19:19:17 +01:00
Denis Merigoux
d71d50ea44 Fixed screenshot mangling 2021-01-03 18:56:03 +01:00
Denis Merigoux
0482acbd01 Fixed incorrect date 2021-01-03 18:52:41 +01:00
Denis Merigoux
606b148c74 Lots of documentation 2020-12-21 16:02:00 +01:00
Denis Merigoux
01b1fdf0b6 Updated formalization 2020-12-21 14:50:45 +01:00
Denis Merigoux
14eec276e3 Change formalization with the exceptions 2020-12-18 19:24:04 +01:00
Denis Merigoux
ef38a6f5be Added compiled formalization pdf 2020-12-14 17:12:12 +01:00
Denis Merigoux
f282d9586b Improved readmes 2020-12-14 10:59:15 +01:00
Denis Merigoux
a4916208ba amount -> money 2020-12-10 09:35:36 +01:00
Denis Merigoux
8005f14ad4 Autoformat 2020-11-20 10:19:21 +01:00
Denis Merigoux
e498e6813b Cleaned formal semantics 2020-11-20 10:17:11 +01:00
Denis Merigoux
f7421d3920 Fixed formalization 2020-11-20 10:12:09 +01:00
Denis Merigoux
7be9abd80a Proved progress and preservation without default functions 2020-11-19 17:54:11 +01:00
Denis Merigoux
f09dc2ab5b Still stuck at substitution preservation 2020-11-18 18:44:14 +01:00
Denis Merigoux
2f1011a7bd Progress 2020-11-18 18:15:36 +01:00
Denis Merigoux
1dfb33f937 Tooling for substitution proof 2020-11-18 17:59:55 +01:00
Denis Merigoux
001ecddde4 More preservation lemmas 2020-11-18 16:26:12 +01:00
Denis Merigoux
a8ff671579 Fixed beta reduction rules for defaults 2020-11-18 15:38:33 +01:00
Denis Merigoux
42a46f417d Progress proven 2020-11-17 21:08:38 +01:00
Denis Merigoux
75562acb1b Checkpoint in proof 2020-11-17 15:54:56 +01:00
Denis Merigoux
88b45c7168 Progress in progress 2020-11-17 14:32:44 +01:00
Denis Merigoux
532365a707 Missing only the default case for progress 2020-11-17 12:15:44 +01:00
Denis Merigoux
891dccb6f8 Trying to prove progress 2020-11-17 11:01:09 +01:00
Denis Merigoux
076e2dce22 Finished writing stepper 2020-11-16 22:51:07 +01:00
Denis Merigoux
6bf935b8e9 Added beginning of F* formalization and fixed paper 2020-11-16 19:34:10 +01:00
Denis Merigoux
fbc07a9258 Complete Catala formalization 2020-11-15 17:33:31 +01:00
Denis Merigoux
a8b30fb0f6 More fixes 2020-11-15 13:02:41 +01:00
Denis Merigoux
a6da799ccf Fixed a number of errors, starting to fall into shape 2020-11-15 12:27:09 +01:00
Denis Merigoux
e334724acc Fix T-ScopeDef 2020-11-14 20:46:53 +01:00
Denis Merigoux
7a6b84e1b8 Fixes and T-ScopeDef 2020-11-14 20:44:48 +01:00
Denis Merigoux
4bf47dbdee Started to describe translation 2020-11-13 18:11:22 +01:00