In this directory, we collect examples and case studies related to our framework.
Each subdirectory contains a formalization of a programming language:
-
SystemF-Simple contains a standalone simplified version of the framework and a formalization of subject reduction for System F.
-
SystemF contains a formalization of subject reduction and progress for System F using the full framework.
-
SystemFSub contains a formalization of subject reduction for SystemF Sub, i.e. System F extended with subtyping bounds.
-
SystemFSub-Alt contains an alternative formalization of subject reduction for SystemF Sub, where subtyping is modelled not as a separate relation, but directly in the typing relation.
-
LambdaPi contains an formalization of subject reduction for a dependently typed lambda calculus with dependent function types, dependent pair types, and an equality type.
-
Patterns contains an formalization of subject reduction for a simply typed lambda calculus with pattern matching, product types, sum types, unit type, and empty type.