Skip to main content
SpringerLink
Log in

An Interpretation of the Fan Theorem in Type Theory

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

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

Included in the following conference series:

Abstract

This article presents a formulation of the fan theorem in Martin-Löf’s type theory. Starting from one of the standard versions of the fan theorem we gradually introduce reformulations leading to a final version which is easy to interpret in type theory. Finally we describe a formal proof of that final version of the fan theorem.

Partially developed during the author’s affiliation to Göteborg University, Sweden.

Basic Research in Computer Science, Centre of the Danish National Research Foundation.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Curry and R. Feys. Combinatory Logic, volume I. North-Holland, 1958. 99

    Google Scholar 

  2. M. Dummett. Elements of Intuitionism. Clarendon Press, Oxford, 1977. 93, 95

    MATH  Google Scholar 

  3. D. Fridlender. Higman’s Lemma in Type Theory. In Types for proofs and programs, Lecture Notes in Computer Science 1512, 1997. 93

    Google Scholar 

  4. W. Howard. The Formulae-as-Types Notion of Construction. In J. Seldin and J. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, London, 1980. 99

    Google Scholar 

  5. L. Magnusson. The Implementation of ALF-a Proof Editor Based on Martin-Löf’ s Monomorphic Type Theory with Explicit Substitution. PhD thesis, Department of Computing Science, Chalmers University of Technology and University of Göteborg, 1994. 94

    Google Scholar 

  6. P. Martin-Löf. Notes on Constructive Mathematics. Almqvist & Wiksell, 1968. 93, 99

    Google Scholar 

  7. P. Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium 1973, pages 73–118, Amsterdam, 1975. North-Holland Publishing Company. 94

    Google Scholar 

  8. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984. 94

    Google Scholar 

  9. B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’ s Type Theory. An Introduction. Oxford University Press, 1990. 94

    Google Scholar 

  10. A. Tasistro. Substitution, Record Types and Subtyping in Type Theory, with Applications to the Theory of Programming. PhD thesis, Department of Computing Science at Chalmers University of Technology and University of Göteborg, 1997. 94

    Google Scholar 

  11. A. Troelstra and D. van Dalen. Constructivism in Mathematics, An Introduction, Volume I. North-Holland, 1988. 93

    Google Scholar 

  12. W. Veldman. Investigations in intuitionistic hierarchy theory. PhD thesis, Katholieke Universiteit te Nijmegen, 1981. 104

    Google Scholar 

  13. W. Veldman. Intuitionistic Proof of the General non-Decidable case of Higman’s Lemma. Personal communication, 1994. 93

    Google Scholar 

  14. W. Veldman. Personal communication, 1998. 94, 104

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000, Aarhus C, Denmark

    Daniel Fridlender

Authors
  1. Daniel Fridlender
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Ludwig-Maximilians-Universität, Institut für Informatik, Oettingenstr. 67, D-80538, München, Germany

    Thorsten Altenkirch  & Bernhard Reus  & 

  2. Technische Universität München, Institut für Informatik, Arcisstr. 21-1528, D-80290, München, Germany

    Wolfgang Naraschewski

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fridlender, D. (1999). An Interpretation of the Fan Theorem in Type Theory. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds) Types for Proofs and Programs. TYPES 1998. Lecture Notes in Computer Science, vol 1657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48167-2_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-48167-2_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66537-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation