Robert Constable ; Wojciech Moczydlowski - Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics

lmcs:1140 - Logical Methods in Computer Science, September 9, 2008, Volume 4, Issue 3 - https://doi.org/10.2168/LMCS-4(3:5)2008
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> SemanticsArticle

Authors: Robert Constable ; Wojciech Moczydlowski

    Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We similarly factor standard set theory, ZFC, into a constructive core, IZF, and axioms of excluded middle and choice. Then we provide the standard set-theoretic semantics in such a way that the constructive core of HOL is mapped into IZF. We use the disjunction, numerical existence and term existence properties of IZF to provide a program extraction capability from proofs in the constructive core. We can implement the disjunction and numerical existence properties in two different ways: one using Rathjen's realizability for IZF and the other using a new direct weak normalization result for IZF by Moczydlowski. The latter can also be used for the term existence property.


    Volume: Volume 4, Issue 3
    Published on: September 9, 2008
    Imported on: January 31, 2007
    Keywords: Computer Science - Logic in Computer Science,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Enabling Large-Scale Coherency Among Mathematical Texts in the NSDL; Funder: National Science Foundation; Code: 0333526
    • Integrating Security and Fault Tolerance in Distributed Systems; Funder: National Science Foundation; Code: 0430161

    Consultation statistics

    This page has been seen 916 times.
    This article's PDF has been downloaded 630 times.