CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 08:47:14 +03:00
Code Issues Projects Releases Wiki Activity
777 Commits 41 Branches 8 Tags 60 MiB
34bab1e3af
Commit Graph

777 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Denis Merigoux
34bab1e3af Fixes #86 2021-03-10 16:51:55 +01:00
Denis Merigoux
04a0e32b74 Fix #85 2021-03-10 16:50:54 +01:00
Denis Merigoux
611ef23fd1 Fix makefile 2021-03-05 19:22:37 +01:00
Denis Merigoux
fdb1975865 Link to paper 2021-03-05 19:19:10 +01:00
Denis Merigoux
baaa79c555 Fixes #78, as well as various improvements 2021-03-05 19:16:56 +01:00
Denis Merigoux
a0511b5885
Merge pull request #80 from CatalaLang/certfication_proof 
Formalization and certfication of the default calculus -> lambda calculus translation
 2021-03-03 13:50:55 +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
1c8acdccf9 Merge branch 'master' into certfication_proof 2021-03-02 18:34:54 +01:00
Denis Merigoux
a4a25f40c2
Merge pull request #82 from CatalaLang/protz_pygments 
For syntax highlighting, use a pygments plugin rather than a fork …
 2021-03-02 18:33:27 +01:00
Denis Merigoux
03774fdfc2 Fixed CI 2021-03-02 18:28:56 +01:00
Denis Merigoux
b0d8ed8a13 Merge branch 'master' into certfication_proof 2021-03-02 16:46:41 +01:00
Denis Merigoux
0259573cd0 Renamed files and makefiles fixes 2021-02-28 18:18:01 +01:00
Denis Merigoux
88d8dd3c31 Generalized plugin scheme for pygments 2021-02-28 18:10:41 +01:00
Denis Merigoux
d28323ae2e Timing information for debug 2021-02-28 11:15:18 +01:00
Jonathan Protzenko
3bcf85bd94 Missing files 2021-02-24 10:55:18 -07:00
Jonathan Protzenko
b206b7a93b For EN syntax highlighting, use a pygments plugin rather than a fork of pygments 2021-02-23 07:53:39 -07: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
fb63c8afc8 Restore tests 2021-02-19 09:09:13 +01:00
Denis Merigoux
e9b134ab79 Progress on section121 after pair programming session 2021-02-18 18:18:34 +01:00