Kripke-style models for typed lambda calculus

Annals of Pure and Applied Logic 51 (1-2):99-124 (1991)
  Copy   BIBTEX

Abstract

Mitchell, J.C. and E. Moggi, Kripke-style models for typed lambda calculus, Annals of Pure and Applied Logic 51 99–124. The semantics of typed lambda calculus is usually described using Henkin models, consisting of functions over some collection of sets, or concrete cartesian closed categories, which are essentially equivalent. We describe a more general class of Kripke-style models. In categorical terms, our Kripke lambda models are cartesian closed subcategories of the presheaves over a poset. To those familiar with Kripke models of modal or intuitionistic logics, Kripke lambda models are likely to seem adequately ‘semantic’. However, when viewed as cartesian closed categories, they do not have the property variously referred to as concreteness, well- pointedness or having enough points. While the traditional lambda calculus proof system is not complete for Henkin models that may have empty types, we prove strong completeness for Kripke models. In fact, every set of equations that is closed under implication is the theory of a single Kripke model. We also develop some properties of logical relations over Kripke structures, showing that every theory is the theory of a model determined by a Kripke equivalence relation over a Henkin model. We discuss cartesian closed categories but present the main definitions and results without the use of category theory

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,202

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.
The lambda calculus: its syntax and semantics.Hendrik Pieter Barendregt - 1981 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
A cut-free Gentzen formulation of basic propositional calculus.Kentaro Kikuchi & Katsumi Sasaki - 2003 - Journal of Logic, Language and Information 12 (2):213-225.
Models of transfinite provability logic.David Fernández-Duque & Joost J. Joosten - 2013 - Journal of Symbolic Logic 78 (2):543-561.
Typed lambda calculus.Henk P. Barendregt, Wil Dekkers & Richard Statman - 1977 - In Jon Barwise & H. Jerome Keisler (eds.), Handbook of Mathematical Logic. North-Holland Pub. Co.. pp. 1091--1132.
Ordinals and ordinal functions representable in the simply typed lambda calculus.N. Danner - 1999 - Annals of Pure and Applied Logic 97 (1-3):179-201.
Alonzo church:his life, his work and some of his miracles.Maía Manzano - 1997 - History and Philosophy of Logic 18 (4):211-232.

Analytics

Added to PP
2014-01-16

Downloads
47 (#322,078)

6 months
12 (#174,629)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Linear Läuchli semantics.R. F. Blute & P. J. Scott - 1996 - Annals of Pure and Applied Logic 77 (2):101-142.
Kripke models and the (in)equational logic of the second-order λ-calculus.Jean Gallier - 1997 - Annals of Pure and Applied Logic 84 (3):257-316.
On church's formal theory of functions and functionals.Giuseppe Longo - 1988 - Annals of Pure and Applied Logic 40 (2):93-133.

Add more citations

References found in this work

Completeness in the theory of types.Leon Henkin - 1950 - Journal of Symbolic Logic 15 (2):81-91.
The lambda calculus: its syntax and semantics.Hendrik Pieter Barendregt - 1981 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Introduction to Higher Order Categorical Logic.J. Lambek & P. J. Scott - 1989 - Journal of Symbolic Logic 54 (3):1113-1114.
The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.

View all 8 references / Add more references