Programs, proofs and parametrized specifications

Iman Poernomo, John N Crossley, Martin Wirsing

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


    In a series of papers we have been using a modification of the ideas of Curry and Howard to obtain reliable programs from formal proofs. In this paper we extend our earlier work by presenting a new approach for constructing correct SML structures and SML functors from CASL structured and parametrized Specifications by extracting the SML programs from constructive proofs of the axioms of the specifications. We provide a novel formal calculus with rules corresponding to the construction and instantiation of parametrized Specifications and then a program extraction procedure which produces SML programs that meet their Specifications.
    Original languageEnglish
    Title of host publicationRecent Trends in Algebraic Development Techniques
    Subtitle of host publication15th International Workshop, WADT 2001 Joint with the CoFI WG Meeting Genova, Italy, April 1-3, 2001 Selected Papers
    EditorsMaura Cerioli, Gianna Reggio
    Place of PublicationBerlin Germany
    Number of pages25
    ISBN (Print)3540431594
    Publication statusPublished - 2001
    EventInternational Workshop on Algebraic Development Techniques 2001 - Genova, Italy
    Duration: 1 Apr 20013 Apr 2001
    Conference number: 15th (Proceedings)

    Publication series

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


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

    Cite this