Protocols between programs and proofs

Iman Poernomo, John N Crossley

    Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

    1 Citation (Scopus)

    Abstract

    In this paper we describe a new protocol that we call the Curry-Howard protocol between a theory and the programs extracted from it. This protocol leads to the expansion of the theory and the production of more powerful programs. The methodology we use for automatically extracting “correct” programs from proofs is a development of the well-known Curry-Howard process. Program extraction has been developed by many authors (see, for example, [9], [5] and [12]), but our presentation is ultimately aimed at a practical, usable system and has a number of novel features. These include

    1.a very simple and natural mimicking of ordinary mathematical practice and likewise the use of established computer programs when we obtain programs from formal proofs, and

    2.a conceptual distinction between programs on the one hand, and proofs of theorems that yield programs on the other.
     
    An implementation of our methodology is the Fred system.1 As an example of our protocol we describe a constructive proof of the well-known theorem that every graph of even parity can be decomposed into a list of disjoint cycles. Given such a graph as input, the extracted program produces a list of the (non-trivial) disjoint cycles as promised.
    Original languageEnglish
    Title of host publicationLogic Based Program Synthesis and Transformation
    Subtitle of host publication10th International Workshop, LOPSTR 2000 London, UK, July 24-28, 2000 Selected Papers
    EditorsKung-Kiu Lau
    Place of PublicationBerlin Germany
    PublisherSpringer
    Pages18-37
    Number of pages20
    ISBN (Print)3540421270
    DOIs
    Publication statusPublished - 2001
    EventInternational Symposium on Logic-based Program Synthesis and Transformation 2000 - London, United Kingdom
    Duration: 24 Jul 200028 Jul 2000
    Conference number: 10th

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume2042
    ISSN (Print)0302-9743

    Conference

    ConferenceInternational Symposium on Logic-based Program Synthesis and Transformation 2000
    Abbreviated titleLOPSTR 2000
    Country/TerritoryUnited Kingdom
    CityLondon
    Period24/07/0028/07/00

    Cite this