Skip to main content
SpringerLink
Log in

An implementation of the Heine-Borel covering theorem in type theory

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1512))

Included in the following conference series:

  • 128 Accesses

Abstract

We describe an implementation, in type theory, of a proof of a pointfree formulation of the Heine-Borel covering theorem for intervals with rational endpoints.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Barendregt. Lambda calculi with types, In S. Abramsky, D.M. Gabbay and T.S.E. Maibaum eds., “Handbook of Logic in Computer Science, Vol. 2”, Oxford University Press, Oxford, 1992.

    Google Scholar 

  2. N.G. de Bruijn. A plea for weaker frameworks, In G. Huet and G. Plotkin eds., “Logical Frameworks”, pp. 40–68, Cambridge University Press, Cambridge, 1991.

    Google Scholar 

  3. J. Cederquist, S. Negri. A constructive proof of the Heine-Borel covering theorem for formal reals, In S. Berardi and M. Coppo eds., “Types for Proofs and Programs”, Lecture Notes in Computer Science 1158, pp. 62–75, Springer-Verlag, 1996.

    Google Scholar 

  4. T. Coquand. An algorithm for type-checking dependent types, Science of Computer Programming 26, pp. 167–177, Elsevier, 1996.

    Google Scholar 

  5. M. Hofmann. A model of intensional Martin-Löf type theory in which unicity of identity proofs does not hold, Technical report, Dept. of Computer Science, University of Edinburgh, 1993.

    Google Scholar 

  6. L. Magnusson. “The Implementation of ALF—a Proof Editor based on Martin-Löf's Monomorphic Type Theory with Explicit Substitution”, Chalmers University of Technology and University of Göteborg, PhD Thesis, 1995.

    Google Scholar 

  7. P. Martin-Löf. An Intuitionistic Theory of Types (1972), To be published in the proceedings of Twenty-five years of Constructive Type Theory, G. Sambin and J. Smith eds., Oxford University Press.

    Google Scholar 

  8. S. Negri, D. Soravia. The continuum as a formal space, Archive for Mathematical Logic, to appear.

    Google Scholar 

  9. S. Owre, N. Shankar, J. M. Rushby. The PVS Specification Language (Beta Release), Computer Science Laboratory, SRI International, Menlo Park, CA 94025, USA, 1993.

    Google Scholar 

  10. J. von Plato. A memorandum on the constructive axioms of linear order, Dept. of Philosophy, University of Helsinki, 1995.

    Google Scholar 

  11. G. Sambin. Intuitionistic formal spaces—a first communication, In D. Skordev ed., “Mathematical logic and its applications”, pp. 187–204, Plenum Press, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Göteborg, S-412 96, Göteborg, Sweden

    Jan Cederquist

Authors
  1. Jan Cederquist
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Eduardo Giménez Christine Paulin-Mohring

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cederquist, J. (1998). An implementation of the Heine-Borel covering theorem in type theory. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0097786

Download citation

  • DOI: https://doi.org/10.1007/BFb0097786

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65137-6

  • Online ISBN: 978-3-540-49562-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation