Extraction of structured programs from specification proofs

John N Crossley, Iman Poernomo, Martin Wirsing

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

    3 Citations (Scopus)


    We present a method using an extended logical system for obtaining programs from specifications written in a sublanguage of CASL. These programs are “correct” in the sense that they satisfy their specifications. The technique we use is to extract programs from proofs in formal logic by techniques due to Curry and Howard. The logical calculus, however, is novel because it adds structural rules corresponding to the standard ways of modifying specifications: translating (renaming), taking unions, and hiding signatures. Although programs extracted by the Curry-Howard process can be very cumbersome, we use a number of simplifications that ensure that the programs extracted are in a language close to a standard high-level programming language. We use this to produce an executable refinement of a given specification and we then provide a method for producing a program module that maximally respects the original structure of the specification. Throughout the paper we demonstrate the technique with a simple example.
    Original languageEnglish
    Title of host publicationRecent Trends in Algebraic Development Techniques
    Subtitle of host publication14th International Workshop, WADT’99 Chateau de Bonas, September 15-18, 1999 Selected Papers
    EditorsDidier Bert, Christine Choppy, Peter Mosses
    Place of PublicationBerlin Germany
    Number of pages19
    ISBN (Print)3540678980
    Publication statusPublished - 2000
    EventInternational Workshop on Algebraic Development Techniques 1999 - Château de Bonas, Toulouse, France
    Duration: 15 Sept 199918 Sept 1999
    Conference number: 14th
    https://link-springer-com.ezproxy.lib.monash.edu.au/book/10.1007/b75154 (Proceedings)

    Publication series

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


    ConferenceInternational Workshop on Algebraic Development Techniques 1999
    Abbreviated titleWADT 1999
    Internet address

    Cite this