Dirk Pattinson ; Mina Mohammadian - Constructive Domains with Classical Witnesses

lmcs:5833 - Logical Methods in Computer Science, March 2, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:19)2021
Constructive Domains with Classical Witnesses

Authors: Dirk Pattinson ; Mina Mohammadian

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.


Volume: Volume 17, Issue 1
Published on: March 2, 2021
Accepted on: November 1, 2020
Submitted on: October 14, 2019
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 182 times.
This article's PDF has been downloaded 94 times.