Pattinson, Dirk and Mohammadian, Mina - Constructive Domains with Classical Witnesses

lmcs:5833 - Logical Methods in Computer Science, March 2, 2021, Volume 17, Issue 1
Constructive Domains with Classical Witnesses

Authors: Pattinson, Dirk and Mohammadian, Mina

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
Submitted on: October 14, 2019
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 80 times.
This article's PDF has been downloaded 36 times.