yellowsquid/cfe-proof.git - [no description]

Age	Commit message (Expand)	Author
2024-01-23	Prove derivations are structurally unique.HEAD master	Chloe Brown
2024-01-23	Add a README detailing progress.	Chloe Brown
2024-01-22	Make more library-like.	Chloe Brown
2021-04-29	Finally prove that e [ μ e / zero ] ≈ μ e.	Chloe Brown
2021-04-24	Cleanup Derivation.cleanup	Chloe Brown
2021-04-24	Reprove properties of the typing judgement.	Chloe Brown
2021-04-24	Modify Fin definitions.	Chloe Brown
2021-04-17	Rework Context one last time.	Chloe Brown
2021-04-12	Remove unnecessary Type construction.	Chloe Brown
2021-04-12	Remove unnecessary comment.	Chloe Brown
2021-04-12	Cleanup Type properties.	Chloe Brown
2021-04-06	Cleanup Type base.	Chloe Brown
2021-04-06	Add lexicographic expression ordering.	Chloe Brown
2021-04-05	Clean up the Expression hierarchy.	Chloe Brown
2021-04-05	Add some missing properties for singleton languages.	Chloe Brown
2021-04-05	Clean-up Language hierarchy.	Chloe Brown
2021-03-29	Introduce < for Languages.	Chloe Brown
2021-03-29	Rename parse to derivation.	Chloe Brown
2021-03-29	Convert to terminating proof using well-founded induction.	Chloe Brown
2021-03-27	Introduce non-terminating proof of derivation existence.	Chloe Brown
2021-03-27	Introduce derivations.	Chloe Brown
2021-03-27	Prove soundness of judgement.soundness	Chloe Brown
2021-03-27	Begin soundness proof.	Chloe Brown
2021-03-27	Prove satisfaction for concatenation.lemma3.5	Chloe Brown
2021-03-25	Prove sequential unique decomposition.	Chloe Brown
2021-03-24	Prove lemma 3.5 (7).	Chloe Brown
2021-03-24	Prove lemma 3.5 (5).	Chloe Brown
2021-03-24	Make progress on lemma 3.5 (4).	Chloe Brown
2021-03-23	Prove substitution into guarded variable.	Chloe Brown
2021-03-23	Replace transfer with shift.	Chloe Brown
2021-03-22	Prove transfer.	Chloe Brown
2021-03-21	Prove judgement weakening.	Chloe Brown
2021-03-20	Separate Context into a different module.	Chloe Brown
2021-03-20	Change judgement to use variable contexts.	Chloe Brown
2021-03-20	Introduce variable contexts.	Chloe Brown
2021-03-16	Change Language definition to respects instead of custom congruence.	Chloe Brown
2021-03-13	Move some properties to Properties.	Chloe Brown
2021-03-13	Add weakening proofs for type judgements.	Chloe Brown
2021-03-05	Add the type judgement	Chloe Brown
2021-03-05	Add type relations.	Chloe Brown
2021-03-05	Add lifted types.	Chloe Brown
2021-03-05	Remove incomplete unrolling proof.	Chloe Brown
2021-03-05	Add lemma 3.5.3.	Chloe Brown
2021-03-05	Prove satisfiability of τε.	Chloe Brown
2021-03-05	Prove satisfiability for τ⊥.	Chloe Brown
2021-03-05	Add base types and operators	Chloe Brown
2021-03-05	Add types and satisfiability	Chloe Brown
2021-03-05	Prove lemma 3.3	Chloe Brown
2021-03-05	Separate out some Language properties.	Chloe Brown
2021-03-05	Complete proofs up to Proposition 3.2 (excluding unrolling)	Chloe Brown