186 Commits

Author	SHA1	Message	Date
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
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