Polymorphic Algorithmic Equality

In order to prove algorithmic equality for a polymorphic lambda-calculus, we establish schemas with alternating assumptions, depending on the type of the variable.

Untyped Algorithmic Equality - Context Subsumption

This example demonstrates Beluga's capacity for automatic context subsumption. If schema W is a prefix of a schema W0, then we can always use a context of schema W0 in place of a context of schema W. Essentially, we allow the user to pass a context of schema W0 where a context with schema W if W0 contains at least as much information as W.

Untyped Algorithmic Equality - Context Relation

Context relationships can be defined explicitly using inductive datatypes. In this proof we use inductive datatypes to establish strengthening and weakening between contexts.

Parallel Reduction

The order of assumptions in a context is important in Beluga. However, sometimes the need to reorder assumptions arises, as is illustrated in the proof of the substitution lemma for algorithmic equality. As in Twelf this kind of proof does not come for free.


This example shows a solution of POPLMARK Challenge, part1A, Transitivity of Subtyping.