Skip to main content
SpringerLink
Log in

An application of constructive completeness

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

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

Included in the following conference series:

  • 260 Accesses

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. Thorsten Altenkirch, Veronica Gaspes, Bengt Nordström, and Björn von Sydow. A User's Guide to ALF. Chalmers University of Technology, Sweden, May 1994.

    Google Scholar 

  2. Jan Cederquist. A machine assisted formalization of pointfree topology in type theory. Licentiate thesis, Chalmers University of Technology and University of Göteborg, Sweden, 1994.

    Google Scholar 

  3. H.C.M. de Swart. An intuitionistically plausible interpretation of intuitionistic logic. Journal of Symbolic Logic, 42:564–578, 1977.

    Google Scholar 

  4. Albert G. Dragalin. An explicit boolean-valued model for non-standard arithmetic. Publ. Math. Drebecen, 42:369–389, 1993.

    Google Scholar 

  5. M. Dummett. Elements of intuitionism. Clarendon Press, Oxford, 1977.

    Google Scholar 

  6. G. Kreisel. On weak completeness of intutionistic predicate logic. Journal of Symbolic logic., 27:139–158, 1962.

    Google Scholar 

  7. H. M. MacNeille. Partially ordered sets. Transactions of AMS, 42, 1937.

    Google Scholar 

  8. Ieke Moerdijk and Erik Palmgren. Minimal models of heyting arithmetik. Technical Report Report U.U.D.M 1995:25, Dept. of Mathematics, Uppsala University, Sweden, June 1995.

    Google Scholar 

  9. Henrik Persson. A formalization of a constructive completeness proof for intuitionistic predicate logic. Draft, Chalmers University of Technology, Göteborg, September 1995.

    Google Scholar 

  10. G. Sambin. Pretopologies and completeness proofs. Journal of Symbolic Logic, 60:861–878, 1995.

    Google Scholar 

  11. Giovanni Sambin. Intuitionistic Formal Spaces — A First Communication. In The Proceedings of Conference on Logic and its Applications, Bulgaria. Plenum Press, 1986.

    Google Scholar 

  12. A. Tarski. Der Aussagenkalkül und die Topologie. Fundamenta Mathematicae, 31:103–134, 1938.

    Google Scholar 

  13. A. S. Troelstra. Choice Sequences, a Chapter of Intuitionistic Mathematics. Clarendon Press, 1977.

    Google Scholar 

  14. A. S. Troelstra and D. van Dalen. Constructivism in Mathematics. An Introduction, volume II. North-Holland, 1988.

    Google Scholar 

  15. Wim Veldman. An intuitionistic completeness theorem for intuitionistic predicate logic. Journal of Symbolic Logic, 41:159–166, 1976.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, Chalmers University of Technology and Univ. of Göteborg, S-41296, Göteborg, Sweden

    Thierry Coquand & Jan M. Smith

Authors
  1. Thierry Coquand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jan M. Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Stefano Berardi Mario Coppo

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coquand, T., Smith, J.M. (1996). An application of constructive completeness. In: Berardi, S., Coppo, M. (eds) Types for Proofs and Programs. TYPES 1995. Lecture Notes in Computer Science, vol 1158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61780-9_63

Download citation

  • DOI: https://doi.org/10.1007/3-540-61780-9_63

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61780-8

  • Online ISBN: 978-3-540-70722-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation