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.
|Number of pages||14|
|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||International Workshop on Types for Proofs and Programs, TYPES 1995|
|Period||5/06/95 → 8/06/95|
|Other||June 5-8, 1995|