No Cover Image

Journal article 1093 views

Typed vs. Untyped realizability

Ulrich Berger Orcid Logo, Tie Hou

Electronic Notes in Theoretical Computer Science, Volume: 286, Pages: 57 - 71

Swansea University Author: Ulrich Berger Orcid Logo

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

DOI (Published version): 10.1016/j.entcs.2012.08.005

Abstract

We study the domain-theoretic semantics of a Church-style typedlambda-calculus with constructors, pattern matching and recursion, and showthat it is closely related to the semantics of its untypedcounterpart. The motivation for this study comes from programextraction from proofs via realizability wh...

Full description

Published in: Electronic Notes in Theoretical Computer Science
Published: 2012
URI: https://cronfa.swan.ac.uk/Record/cronfa14368
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T12:12:07Z
last_indexed 2018-02-09T04:45:45Z
id cronfa14368
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2011-10-01T00:00:00.0000000</datestamp><bib-version>v2</bib-version><id>14368</id><entry>2013-02-25</entry><title>Typed vs. Untyped realizability</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>2013-02-25</date><deptcode>SCS</deptcode><abstract>We study the domain-theoretic semantics of a Church-style typedlambda-calculus with constructors, pattern matching and recursion, and showthat it is closely related to the semantics of its untypedcounterpart. The motivation for this study comes from programextraction from proofs via realizability where one has the choice ofextracting typed or untyped terms from proofs. Our result shows thatunder a certain regularity condition, the choice is irrelevant. Theregularity condition is that in every use of a fixed point type fixalpha.rho, alpha occurs only positively in rho.</abstract><type>Journal Article</type><journal>Electronic Notes in Theoretical Computer Science</journal><volume>286</volume><journalNumber></journalNumber><paginationStart>57</paginationStart><paginationEnd>71</paginationEnd><publisher/><placeOfPublication/><issnPrint/><issnElectronic/><keywords>Scott domain, typed and untyped &#x3BB;-calculus, program extraction, logical relation, realizability</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2012</publishedYear><publishedDate>2012-12-31</publishedDate><doi>10.1016/j.entcs.2012.08.005</doi><url/><notes>Proceedings of MFPS XXVIII, Bath, 6-9 June 2012</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2011-10-01T00:00:00.0000000</lastEdited><Created>2013-02-25T15:18:24.4883560</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 2011-10-01T00:00:00.0000000 v2 14368 2013-02-25 Typed vs. Untyped realizability 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2013-02-25 SCS We study the domain-theoretic semantics of a Church-style typedlambda-calculus with constructors, pattern matching and recursion, and showthat it is closely related to the semantics of its untypedcounterpart. The motivation for this study comes from programextraction from proofs via realizability where one has the choice ofextracting typed or untyped terms from proofs. Our result shows thatunder a certain regularity condition, the choice is irrelevant. Theregularity condition is that in every use of a fixed point type fixalpha.rho, alpha occurs only positively in rho. Journal Article Electronic Notes in Theoretical Computer Science 286 57 71 Scott domain, typed and untyped λ-calculus, program extraction, logical relation, realizability 31 12 2012 2012-12-31 10.1016/j.entcs.2012.08.005 Proceedings of MFPS XXVIII, Bath, 6-9 June 2012 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2011-10-01T00:00:00.0000000 2013-02-25T15:18:24.4883560 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Tie Hou 2
title Typed vs. Untyped realizability
spellingShingle Typed vs. Untyped realizability
Ulrich Berger
title_short Typed vs. Untyped realizability
title_full Typed vs. Untyped realizability
title_fullStr Typed vs. Untyped realizability
title_full_unstemmed Typed vs. Untyped realizability
title_sort Typed vs. Untyped realizability
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 Electronic Notes in Theoretical Computer Science
container_volume 286
container_start_page 57
publishDate 2012
institution Swansea University
doi_str_mv 10.1016/j.entcs.2012.08.005
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
document_store_str 0
active_str 0
description We study the domain-theoretic semantics of a Church-style typedlambda-calculus with constructors, pattern matching and recursion, and showthat it is closely related to the semantics of its untypedcounterpart. The motivation for this study comes from programextraction from proofs via realizability where one has the choice ofextracting typed or untyped terms from proofs. Our result shows thatunder a certain regularity condition, the choice is irrelevant. Theregularity condition is that in every use of a fixed point type fixalpha.rho, alpha occurs only positively in rho.
published_date 2012-12-31T03:16:29Z
_version_ 1763750329091883008
score 11.013619

Similar Items