Contextual equivalence for inductive definitions with binders in higher order typed functional programming
From MaRDI portal
Publication:2875221
DOI10.1017/S0956796813000245zbMath1300.68017OpenAlexW2093321451MaRDI QIDQ2875221
Matthew R. Lakin, Andrew M. Pitts
Publication date: 14 August 2014
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796813000245
Cites Work
- Unnamed Item
- Unnamed Item
- Equivariant unification
- A new approach to abstract syntax with variable binding
- Capture-avoiding substitution as a nominal algebra
- External and internal syntax of the \(\lambda \)-calculus
- The undecidability of the second-order unification problem
- The Qu-Prolog unification algorithm: formalisation and correctness
- Nominal unification
- Nominal logic, a first order theory of names and binding
- Proving congruence of bisimulation in functional programming languages
- Some lambda calculus and type theory formalized
- Encoding abstract syntax without fresh names
- A canonical locally named representation of binding
- On a monadic semantics for freshness
- A lattice-theoretical fixpoint theorem and its applications
- A needed narrowing strategy
- Alpha-structural recursion and induction
- Proving termination with multiset orderings
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
- Equivalence in functional languages with effects
- A proof theory for generic judgments
- Howe's method for higher-order languages
- Proceedings of the eighth ACM SIGPLAN international conference on Functional programming
- Proceedings of the 12th ACM SIGPLAN international conference on Functional programming
- Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
This page was built for publication: Contextual equivalence for inductive definitions with binders in higher order typed functional programming
