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 |
|
Denis Merigoux
|
6389bee394
|
Beginning of scope language
|
2020-11-13 12:38:57 +01:00 |
|
Denis Merigoux
|
e78643b6ef
|
Better introductions
|
2020-11-13 11:46:37 +01:00 |
|
Denis Merigoux
|
b51eb51f45
|
Finished default calculus section
|
2020-11-13 09:52:42 +01:00 |
|
Denis Merigoux
|
6e6e15b2bb
|
Revamped formalization
|
2020-11-12 19:37:32 +01:00 |
|
Denis Merigoux
|
87cf52e16f
|
Merge branch 'master' into formalization
|
2020-11-12 16:52:18 +01:00 |
|
Nicolas Chataing
|
f356fd9a1e
|
Rework defaut calculus
|
2020-11-01 09:31:36 +01:00 |
|
Denis Merigoux
|
8c22b8e47a
|
Change screenshot with English
|
2020-10-31 21:06:51 +01:00 |
|
Nicolas Chataing
|
9e19b38cb4
|
Include catala formalisation
|
2020-10-13 14:59:41 +02:00 |
|
Denis Merigoux
|
9b0573f12c
|
Added revised square logo
|
2020-05-15 15:47:40 +02:00 |
|
Denis Merigoux
|
8e5743c6c6
|
Added scope inclusion in surface language syntax
|
2020-05-14 23:31:57 +02:00 |
|
Denis Merigoux
|
58e1a76a78
|
Added logo proposal
|
2020-05-14 22:53:42 +02:00 |
|
Denis Merigoux
|
c270c5fbab
|
Removed optional condition on meta assertions
|
2020-04-25 14:21:26 +02:00 |
|
Denis Merigoux
|
eb801fe593
|
More more doc
|
2020-04-17 16:22:20 +02:00 |
|
Denis Merigoux
|
72bf4d01cb
|
Big refactoring, better pdf build reproducibility
|
2020-04-17 12:29:30 +02:00 |
|
Denis Merigoux
|
ae5cf4ad22
|
Lax improvements
|
2020-04-16 11:25:27 +02:00 |
|
Denis Merigoux
|
564a332c3b
|
Added thin wrapper that just shows code
|
2020-04-15 15:10:27 +02:00 |
|