summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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
2021-02-18Another redefinition of Language.Chloe Brown
2021-02-08Make languages records with more properties.Chloe Brown
2021-01-28Define induced posets.Chloe Brown
2021-01-23Add basic properties of ≤Chloe Brown
2021-01-23Define expression equivalence.Chloe Brown
2021-01-23Define semantics of expressions.Chloe Brown
2021-01-23Define languages.Chloe Brown
2021-01-23Define expressionsChloe Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 20:31:50 +0000