Journal article 1334 views
A realizability interpretation of Church's simple theory of types
,
TIE HOU
Mathematical Structures in Computer Science, Volume: 27, Issue: 8, Pages: 1364 - 1385
Swansea University Author:
Ulrich Berger
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1017/s0960129516000104
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...
| Published in: | Mathematical Structures in Computer Science |
|---|---|
| ISSN: | 0960-1295 1469-8072 |
| Published: |
Cambridge University Press (CUP)
2017
|
| 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 |
| College: |
Faculty of Science and Engineering |
| Issue: |
8 |
| Start Page: |
1364 |
| End Page: |
1385 |