summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2024-01-23Prove derivations are structurally unique.HEADmasterChloe Brown
2024-01-23Add a README detailing progress.Chloe Brown
2024-01-22Make more library-like.Chloe Brown
Add an `agda-lib` and an `Everything` file.
2021-04-29Finally prove that e [ μ e / zero ] ≈ μ e.Chloe Brown
Complete proof of generator.
2021-04-24Cleanup Derivation.cleanupChloe Brown
2021-04-24Reprove properties of the typing judgement.Chloe Brown
2021-04-24Modify Fin definitions.Chloe Brown
2021-04-17Rework Context one last time.Chloe Brown
2021-04-12Remove unnecessary Type construction.Chloe Brown
2021-04-12Remove unnecessary comment.Chloe Brown
2021-04-12Cleanup Type properties.Chloe Brown
2021-04-06Cleanup Type base.Chloe Brown
2021-04-06Add lexicographic expression ordering.Chloe Brown
2021-04-05Clean up the Expression hierarchy.Chloe Brown
2021-04-05Add some missing properties for singleton languages.Chloe Brown
2021-04-05Clean-up Language hierarchy.Chloe Brown
2021-03-29Introduce < for Languages.Chloe Brown
Move around some definitions.
2021-03-29Rename parse to derivation.Chloe Brown
2021-03-29Convert to terminating proof using well-founded induction.Chloe Brown
2021-03-27Introduce non-terminating proof of derivation existence.Chloe Brown
2021-03-27Introduce derivations.Chloe Brown
2021-03-27Prove soundness of judgement.soundnessChloe Brown
2021-03-27Begin soundness proof.Chloe Brown
2021-03-27Prove satisfaction for concatenation.lemma3.5Chloe Brown
2021-03-25Prove sequential unique decomposition.Chloe Brown
Fix faulty definition of flast set.
2021-03-24Prove lemma 3.5 (7).Chloe Brown
2021-03-24Prove lemma 3.5 (5).Chloe Brown
2021-03-24Make progress on lemma 3.5 (4).Chloe Brown
2021-03-23Prove substitution into guarded variable.Chloe Brown
2021-03-23Replace transfer with shift.Chloe Brown
Prove substitution in the unguarded context.
2021-03-22Prove transfer.Chloe Brown
2021-03-21Prove judgement weakening.Chloe Brown
2021-03-20Separate Context into a different module.Chloe Brown
2021-03-20Change judgement to use variable contexts.Chloe Brown
Add some useful context transformations.
2021-03-20Introduce variable contexts.Chloe Brown
2021-03-16Change Language definition to respects instead of custom congruence.Chloe Brown
2021-03-13Move some properties to Properties.Chloe Brown
2021-03-13Add weakening proofs for type judgements.Chloe Brown
2021-03-05Add the type judgementChloe Brown
2021-03-05Add type relations.Chloe Brown
2021-03-05Add lifted types.Chloe Brown
2021-03-05Remove incomplete unrolling proof.Chloe Brown
2021-03-05Add lemma 3.5.3.Chloe Brown
2021-03-05Prove satisfiability of τε.Chloe Brown
There is a small error in the paper. It claims that L⊨τε if and only if L≈{ε}. However, from `⊨-anticongˡ` and `≤-min`, we have ∅⊨{ε}.
2021-03-05Prove satisfiability for τ⊥.Chloe Brown
2021-03-05Add base types and operatorsChloe Brown
2021-03-05Add types and satisfiabilityChloe Brown
2021-03-05Prove lemma 3.3Chloe Brown
2021-03-05Separate out some Language properties.Chloe Brown
2021-03-05Complete proofs up to Proposition 3.2 (excluding unrolling)Chloe Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 22:46:36 +0000