On Definability and Normalization by Evaluation in the Logical Framework

Abstract

The question of definability asks to characterise what objects of the meta-theory are definable by a given calculus; for example, the untyped -calculus characterises exactly the Turing-computable functions. This thesis gives a characterisation of LF-definability—definability in a variant of the Edinburgh Logical Framework—in terms of a notion of Kripke predicates. The constructions in this thesis are heavily inspired by, and generalise, those by Jung and Tiuryn, who gave a definability result for the simply-typed -calculus in ‘A New Characterization of Lambda Definability’.