Journal article 1086 views
Typed vs. Untyped realizability
,
Tie Hou
Electronic Notes in Theoretical Computer Science, Volume: 286, Pages: 57 - 71
Swansea University Author:
Ulrich Berger
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...
| 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!
|
| 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. |
|---|---|
| Item Description: |
Proceedings of MFPS XXVIII, Bath, 6-9 June 2012 |
| Keywords: |
Scott domain, typed and untyped λ-calculus, program extraction, logical relation, realizability |
| College: |
Faculty of Science and Engineering |
| Start Page: |
57 |
| End Page: |
71 |