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 WitnessesArticle

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

    1 Document citing this article

    Consultation statistics

    This page has been seen 1067 times.
    This article's PDF has been downloaded 192 times.