A Constructive Proof of the Heine-Borel Covering Theorem for Formal Reals

Stefano Berardi (Editor), J.G. Cederquist, Mario Coppo (Editor), Sara Negri

    Research output: Contribution to conferencePaperpeer-review

    18 Citations (Scopus)
    181 Downloads (Pure)

    Abstract

    The continuum is here presented as a formal space by means of a finitary inductive definition. In this setting a constructive proof of the Heine-Borel covering theorem is given.
    Original languageUndefined
    Pages62-75
    Number of pages14
    DOIs
    Publication statusPublished - Jun 1995
    EventInternational Workshop on Types for Proofs and Programs, TYPES 1995 - Torino, Italy
    Duration: 5 Jun 19958 Jun 1995

    Workshop

    WorkshopInternational Workshop on Types for Proofs and Programs, TYPES 1995
    Period5/06/958/06/95
    OtherJune 5-8, 1995

    Keywords

    • EWI-1150
    • IR-56272

    Cite this