Matching typed and untyped realizability

Research output: Contribution to journalArticlepeer-review

Abstract

Realizability interpretations of logics are given by saying what it means for computational objects of some kind to realize logical formulae. The computational objects in question might be drawn from an untyped universe of computation, such as a partial combinatory algebra, or they might be typed objects such as terms of a PCF-style programming language. In some instances, one can show that a particular untyped realizability interpretation matches a particular typed one, in the sense that they give the same set of realizable formulae. In this case, we have a very good fit indeed between the typed language and the untyped realizability model — we refer to this condition as (constructive) logical full abstraction.

We give some examples of this situation for a variety of extensions of PCF. Of particular interest are some models that are logically fully abstract for typed languages including non-functional features. Our results establish connections between what is computable in various programming languages and what is true inside various realizability toposes. We consider some examples of logical formulae to illustrate these ideas, in particular their application to exact real-number computability.
Original languageEnglish
Pages (from-to)74-100
Number of pages27
JournalElectronic Notes in Theoretical Computer Science
Volume23
Issue number1
DOIs
Publication statusPublished - 1999

Fingerprint

Dive into the research topics of 'Matching typed and untyped realizability'. Together they form a unique fingerprint.

Cite this