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

Stefano Berardi; J.G. Cederquist; Mario Coppo; Sara Negri

doi:10.1007/3-540-61780-9_62

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 conference › Paper › peer-review

20 Citations (Scopus)

360 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 language	Undefined
Pages	62-75
Number of pages	14
DOIs	https://doi.org/10.1007/3-540-61780-9_62
Publication status	Published - Jun 1995
Event	International Workshop on Types for Proofs and Programs, TYPES 1995 - Torino, Italy Duration: 5 Jun 1995 → 8 Jun 1995

Workshop

Workshop	International Workshop on Types for Proofs and Programs, TYPES 1995
Abbreviated title	TYPES
Country/Territory	Italy
City	Torino
Period	5/06/95 → 8/06/95

Keywords

EWI-1150
IR-56272

Access to Document

10.1007/3-540-61780-9_62

cederquist96constructive

Cite this

@conference{84cb46d61df0479bad6f07a9540ae5e7,

title = "A Constructive Proof of the Heine-Borel Covering Theorem for Formal Reals",

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.",

keywords = "EWI-1150, IR-56272",

author = "Stefano Berardi and J.G. Cederquist and Mario Coppo and Sara Negri",

note = "Imported from DIES; International Workshop on Types for Proofs and Programs, TYPES 1995 ; Conference date: 05-06-1995 Through 08-06-1995",

year = "1995",

month = jun,

doi = "10.1007/3-540-61780-9\_62",

language = "Undefined",

pages = "62--75",

}

TY - CONF

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

AU - Cederquist, J.G.

AU - Negri, Sara

A2 - Berardi, Stefano

A2 - Coppo, Mario

N1 - Imported from DIES

PY - 1995/6

Y1 - 1995/6

N2 - 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.

AB - 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.

KW - EWI-1150

KW - IR-56272

U2 - 10.1007/3-540-61780-9_62

DO - 10.1007/3-540-61780-9_62

M3 - Paper

SP - 62

EP - 75

T2 - International Workshop on Types for Proofs and Programs, TYPES 1995

Y2 - 5 June 1995 through 8 June 1995

ER -