Journal of Functional Programming

Articles

Contextual equivalence for inductive definitions with binders in higher order typed functional programming

MATTHEW R. LAKINa1 p1 and ANDREW M. PITTSa1

a1 Computer Laboratory, University of Cambridge, 15 JJ Thomson Avenue, Cambridge CB3 0FD, UK (e-mail: Matthew.Lakin@cl.cam.ac.uk, Andrew.Pitts@cl.cam.ac.uk)

Abstract

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 the conference paper (Lakin, M. R. & Pitts, A. M. (2009) Resolving inductive definitions with binders in higher-order typed functional programming. In Proceedings of the 18th European Symposium on Programming (ESOP 2009), Castagna, G. (ed), Lecture Notes in Computer Science, vol. 5502. Berlin, Germany: Springer-Verlag, pp. 47–61) and draws on material from the first author's PhD thesis (Lakin, M. R. (2010) An Executable Meta-Language for Inductive Definitions with Binders. University of Cambridge, UK).

(Online publication December 13 2013)

Correspondence

p1 Current address: Department of Computer Science, University of New Mexico, Albuquerque, NM 87131-0001, USA