We discuss connections of typed λ-calculus and cartesian closure and prove equivalence of the theories ‘up to abstraction’. This is a working out of ideas of Scott and Lambeck but in an abstract data type environment. The results serve as a basis for the discussion of higher order specifications. We demonstrate that higher order equations based on λ-calculus are more appropriate if the equivalence of λ-calculus and cartesian closure is to be preserved. We construct higher order theories for higher order specifications. For higher order models we discuss existence of initial models and completeness of higher order theories.
CITATION STYLE
Poigné, A. (1984). Higher order data structures- cartesian closure versus λ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 166 LNCS, pp. 174–185). Springer Verlag. https://doi.org/10.1007/3-540-12920-0_16
Mendeley helps you to discover research relevant for your work.