No Cover Image

Journal article 1334 views

A realizability interpretation of Church's simple theory of types

Ulrich Berger Orcid Logo, TIE HOU

Mathematical Structures in Computer Science, Volume: 27, Issue: 8, Pages: 1364 - 1385

Swansea University Author: Ulrich Berger Orcid Logo

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

Check full text

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...

Full description

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!
first_indexed 2015-05-27T02:10:54Z
last_indexed 2021-01-29T03:36:27Z
id cronfa21694
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2021-01-28T16:07:41.7791139</datestamp><bib-version>v2</bib-version><id>21694</id><entry>2015-05-26</entry><title>A realizability interpretation of Church's simple theory of types</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2015-05-26</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Mathematical Structures in Computer Science</journal><volume>27</volume><journalNumber>8</journalNumber><paginationStart>1364</paginationStart><paginationEnd>1385</paginationEnd><publisher>Cambridge University Press (CUP)</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint>0960-1295</issnPrint><issnElectronic>1469-8072</issnElectronic><keywords>Realizability, Church&amp;apos;s simple theory of types, Program extraction</keywords><publishedDay>1</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2017</publishedYear><publishedDate>2017-12-01</publishedDate><doi>10.1017/s0960129516000104</doi><url>http://dx.doi.org/10.1017/s0960129516000104</url><notes>Special issue for the international conference "Constructivity, Computability, Continuity - from Logic to Algorithms (CCC 2013)"</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2021-01-28T16:07:41.7791139</lastEdited><Created>2015-05-26T14:39:13.5895071</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>1</order></author><author><firstname>TIE</firstname><surname>HOU</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2021-01-28T16:07:41.7791139 v2 21694 2015-05-26 A realizability interpretation of Church's simple theory of types 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2015-05-26 SCS 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. Journal Article Mathematical Structures in Computer Science 27 8 1364 1385 Cambridge University Press (CUP) 0960-1295 1469-8072 Realizability, Church&apos;s simple theory of types, Program extraction 1 12 2017 2017-12-01 10.1017/s0960129516000104 http://dx.doi.org/10.1017/s0960129516000104 Special issue for the international conference "Constructivity, Computability, Continuity - from Logic to Algorithms (CCC 2013)" COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2021-01-28T16:07:41.7791139 2015-05-26T14:39:13.5895071 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 TIE HOU 2
title A realizability interpretation of Church's simple theory of types
spellingShingle A realizability interpretation of Church's simple theory of types
Ulrich Berger
title_short A realizability interpretation of Church's simple theory of types
title_full A realizability interpretation of Church's simple theory of types
title_fullStr A realizability interpretation of Church's simple theory of types
title_full_unstemmed A realizability interpretation of Church's simple theory of types
title_sort A realizability interpretation of Church's simple theory of types
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
TIE HOU
format Journal article
container_title Mathematical Structures in Computer Science
container_volume 27
container_issue 8
container_start_page 1364
publishDate 2017
institution Swansea University
issn 0960-1295
1469-8072
doi_str_mv 10.1017/s0960129516000104
publisher Cambridge University Press (CUP)
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://dx.doi.org/10.1017/s0960129516000104
document_store_str 0
active_str 0
description 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.
published_date 2017-12-01T03:25:47Z
_version_ 1763750914028470272
score 11.035634

Similar Items