No Cover Image

Journal article 589 views

A realizability interpretation of Church's simple theory of types / Ulrich, Berger

Mathematical Structures in Computer Science, Pages: 1 - 22

Swansea University Author: Ulrich, Berger

Full text not available from this repository: check for access using links below.

Abstract

We present a realizability interpretation of an intuitionistic version of Church's Simple Theory of Types (CST) which can be viewed as a formalization of intuitionistic higher-order logic. Although definable in CST we include operators for monotone induction and coinduction and provide simple r...

Full description

Published in: Mathematical Structures in Computer Science
ISSN: 1469-8072
Published: 2016
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa21694
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: We present a realizability interpretation of an intuitionistic version of Church's Simple Theory of Types (CST) which can be viewed as a formalization of intuitionistic higher-order logic. Although definable in CST we include operators for monotone induction and coinduction and provide simple realizers for them. Realizers are formally represented in an untyped lambda-calculus with pairing and case-construct. We introduce a general notion of interpretation of one instance of the simply typed lambda calculus in another, and define realizability as an instance of such an interpretation. In this way, important syntactic properties of realizability (e.g. being well-behaved w.r.t. substitution) can be proven elegantly on an abstract lambda-calculus level.
Item Description: Special issue for the international conference "Constructivity, Computability, Continuity - from Logic to Algorithms (CCC 2013)"
Keywords: Realizability, Church's simple theory of types, Program extraction
Start Page: 1
End Page: 22