Fixed Points and Extensionality in Typed Functional Programming Languages

摘要

We consider the interaction of recursion with extensional data types in severaltyped functional programming languages based on the simply-typed lambda calculus. Our main results concern the relation between the equational proof systems for reasoning about terms and the operational semantics for evaluating programs. We also present several results about the expressivity of the languages, compared according to both the functions and the data types definable in them. The methods used are those of classical lambda calculus and category theory.