[Prev][Next][Index][Thread]
talk for Logic Colloq '88
Here are my current title and abstract.
Constructive comments appreciated.
-----
Typed Lambda Calculus and Logical Relations
John C. Mitchell
Department of Computer Science
Stanford University
Abstract
Although typed lambda calculus has been studied for over
50 years, recent applications to computer science have
led to a shift in perspective, and therefore new technical
results. For example, classical studies have focused on
versions of the calculus with nonempty sets of individuals
(e.g., the natural numbers) and truth values as basic
types. However, in programming languages, it is common to
declare new data types, or define types by logical formulas.
In this context, we are not guaranteed that all types
are nonempty. Accommodating this seemingly small change
leads to an entirely new perspective on the model theory
of the calculus. In particular, basic theorems such as
deductive completeness work out more naturally in the
framework of intuitionistic logic. This meshes well with
computer science motivations, since categories of
domains and other natural spaces of computable values
are easily embedded in intuitionistic logics (toposes).
Logical relations are a fundamental technique in the proof
theory and model theory of typed lambda calculus. For example,
normalization (every typed lambda term simplifies to a
normal form) and various completeness theorems are easily
proved. In addition, logical relations are essential to
the computer science theory of representation independence,
a theory meant to capture the idea that compiler writers
may represent basic values in whatever way they find convenient
(and, presumably, efficient), as long as the correct
operational behavior is guaranteed. We will see that logical
relations may be formulated in either a classical or
intuitionistic framework.