The following pages link to (Q2871861):
Displaying 11 items.
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- Nominal abstraction (Q617715) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← links)
- Completeness in PVS of a nominal unification algorithm (Q1744405) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols (Q1744440) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols (Q2424886) (← links)
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention (Q5022932) (← links)
- Nominal Sets in Agda - A Fresh and Immature Mechanization (Q6118749) (← links)
