Journal article 3 views
Constructive Domains with Classical Witnesses
Logical Methods in Computer Science, Volume: 17, Issue: 1, Pages: 19:1 - 19:30
Swansea University Author:
Mina Cyrus
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.23638/LMCS-17(1:19)2021
Abstract
We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain ba...
| Published in: | Logical Methods in Computer Science |
|---|---|
| ISSN: | 1860-5974 |
| Published: |
Logical Methods in Computer Science e.V.
2021
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa68135 |
| Abstract: |
We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain base and construct a completion. We then investigate continuity with respect to the Scott topology, and present a construction of the function space. We then discuss our main motivating example in detail, and instantiate our theory to real numbers that we conceptualise as the total elements of the completion of the predomain of rational intervals, and prove a representation theorem that precisely delineates the class of representable continuous functions. |
|---|---|
| Keywords: |
Domain Theory, Constructive Mathematics, Real Number Computation, Predomain Base, Function Spaces |
| College: |
Faculty of Science and Engineering |
| Issue: |
1 |
| Start Page: |
19:1 |
| End Page: |
19:30 |