Contextual Equivalence for Inductive Definitions
with Binders in Higher-Order Typed Functional Programming
Correct handling of names and binders is an important issue in
meta-programming. This paper presents an embedding of constraint
logic programming into the αML functional programming language,
which provides a provably correct means of implementing proof search
computations over inductive definitions involving names and binders
modulo α-equivalence. We show that the execution of proof
search in the αML operational semantics is sound and complete
with regard to the model-theoretic semantics of formulae, and develop
a theory of contextual equivalence for the subclass of αML
expressions which correspond to inductive definitions and
formulae. In particular, we prove that αML expressions which
denote inductive definitions are contextually equivalent precisely
when those inductive definitions have the same model-theoretic
semantics. This paper is a revised and extended version of a
conference paper (Lakin & Pitts,
2009) and draws on material from the first author’s Ph.D. thesis
(Lakin,
2010).