Program extraction from large proof developments

L. Cruz-Filipe, B.A.W. Spitters

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

    11 Citations (Scopus)

    Abstract

    It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time and effort to implement these algorithms on a computer; moreover, one runs the risk of making mistakes in the process. From a fully formalized constructive proof one can automatically obtain a computer implementation of such an algorithm together with a proof that the program is correct. As an example we consider the fundamental theorem of algebra which states that every non-constant polynomial has a root. This theorem has been fully formalized in the Coq proof assistant. Unfortunately, when we first tried to extract a program, the computer ran out of resources. We will discuss how we used logical techniques to make it possible to extract a feasible program. This example is used as a motivation for a broader perspective on how the formalization of mathematics should be done with program extraction in mind.
    Original languageEnglish
    Title of host publicationTheorem Proving in Higher Order Logics (Proceedings 16th International Conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003)
    EditorsD.A. Basin, B. Wolff
    Place of PublicationBerlin
    PublisherSpringer
    Pages205-220
    ISBN (Print)3-540-40664-6
    DOIs
    Publication statusPublished - 2003

    Publication series

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

    Fingerprint

    Dive into the research topics of 'Program extraction from large proof developments'. Together they form a unique fingerprint.

    Cite this