Skip to main content
SpringerLink
Log in

Recent Results in Type Theory and Their Relationship to Automath

  • Chapter
Thirty Five Years of Automating Mathematics

Part of the book series: Applied Logic Series ((APLS,volume 28))

  • 333 Accesses

Abstract

The notion of a telescope is basic to Automath’s theory structure; telescopes provide the context for theorems. A dependent record type is an internal version of a telescope and is used in to define theories. This paper shows how A. Kopylov defines these record types in terms of dependent intersections, a new type constructor.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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.

Bibliography

  1. M. Abadi and L. Cardelli. A Theory of Objects. Springer, 1996.

    Google Scholar 

  2. S. F. Allen. A Non-type-theoretic Definition of Martin-Löf’s Types. In D. Gries, editor, Proceedings of the 2 IEEE Symposium on Logic in Computer Science, pages 215–224. IEEE Computer Society Press, June 1987.

    Google Scholar 

  3. S. F. Allen. From dy/dx to []p: a matter of notation. In Proceedings of the Conference on User Interfaces for Theorem Provers, Eindhoven, The Netherlands, 1998.

    Google Scholar 

  4. H. Barendregt and H. Geuvers. Proof-assistants using dependent type systems. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 1149–1238. Elsevier, 2001.

    Google Scholar 

  5. G. Betarte and A. Tasistro. Extension of Martin Löf’s type theory with record types and subtyping. In Twenty-Five Years of Constructive Type Theory, chapter 2, pages 21–39. Oxford Science Publications, 1999.

    Google Scholar 

  6. R. Bloo, F. Kamareddine, and R. Nederpelt. The Barendregt cube with definitions and generalised reduction. Information and Computation, 126(2):123143, 1996.

    Google Scholar 

  7. R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendier, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the NuPRL Development System. Prentice-Hall, NJ, 1986.

    Google Scholar 

  8. R. L. Constable and J. Hickey. NuPRL’s class theory and its applications. In F. L. Bauer and R. Steinbrueggen, editors, Foundations of Secure Computation, NATO ASI Series, Series F: Computer and System Sciences, pages 91116. IOS Press, 2000.

    Google Scholar 

  9. R. L. Constable, P. Jackson, P. Naumov, and J. Uribe. Constructively formalizing automata theory. Proof, Language and Interaction: Essays in Honour of Robert Milner, 1998.

    Google Scholar 

  10. T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76: 95–120, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  11. T. Coquand and C. Paulin-Mohring. Inductively defined types, preliminary version. In COLOG ‘88, International Conference on Computer Logic, volume 417 of Lecture Notes in Computer Science, pages 50–66. Springer, Berlin, 1990.

    Chapter  Google Scholar 

  12. N. G. de Bruijn. The mathematical language Automath: its usage and some of its extensions. In J. P. Seldin and J. R. Hindley, editors, Symposium on Automatic Demonstration, volume 125 of Lecture Notes in Mathematics, pages 29–61. Springer-Verlag, 1970.

    Google Scholar 

  13. N. G. de Bruijn. A survey of the project Automath. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589–606. Academic Press, 1980.

    Google Scholar 

  14. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant User’s Guide. INRIA, Version 5. 8, 1993.

    Google Scholar 

  15. A. Franke and M. Kohlhase. MATUWEB, an agent-based communication layer for distributed automated theorem proving. In Ganzinger [Ganzinger, 1999 ].

    Google Scholar 

  16. H. Ganzinger, editor. Proceedings of the 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, Berlin, July 7–10 1999. Trento, Italy.

    Google Scholar 

  17. H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg. The algebraic hierarchy of the FTA project. In Calculemus 2001 Proceedings, Siena, Italy, 2001.

    Google Scholar 

  18. J.-Y. Girard. Une extension de l’interpretation de Gödel a l’analyse, et son application a l’elimination des coupures dans l’analyse et la theorie des types. In 2nd Scandinavian Logic Symposium, pages 63–69. Springer-Verlag, NY, 1971.

    Chapter  Google Scholar 

  19. W. Howard. The formulas-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 479–490. Academic Press, NY, 1980.

    Google Scholar 

  20. D. J. Howe. Equality in lazy computation systems. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pages 198–203, Asilomar Conference Center, Pacific Grove, California, June 1989. IEEE, IEEE Computer Society Press.

    Google Scholar 

  21. D. J. Howe. Semantic foundations for embedding HOL in NuPRL. In M. Wirsing and M. Nivat, editors, Algebraic Methodology and Software Technology, volume 1101 of Lecture Notes in Computer Science, pages 85–101. Springer-Verlag, Berlin, 1996.

    Google Scholar 

  22. K. Jensen and N. Wirth. PASCAL user manual and report. Springer-Verlag, New York, 1974.

    Google Scholar 

  23. F. Kamareddine and R. P. Nederpelt. A unified approach to type theory through a refined lambda-calculus. Theoretical Computer Science, 136 (1): 183–216, December 1994.

    Article  MathSciNet  MATH  Google Scholar 

  24. A. Kopylov. Dependent intersection: A new way of defining records in type theory. In Proceedings of 18th IEEE Symposium on Logic in Computer Science, 2003. To appear.

    Google Scholar 

  25. P. Martin-Löf. An intuitionistic theory of types: Predicative part. In Logic Colloquium ‘73, pages 73–118. North-Holland, Amsterdam, 1973.

    Google Scholar 

  26. P. Martin-Löf. Intuitionistic Type Theory. Number 1 in Studies in Proof Theory, Lecture Notes. Bibliopolis, Napoli, 1984.

    Google Scholar 

  27. R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer. Selected Papers on Automath, volume 133 of Studies in Logic and The Foundations of Mathematics. Elsevier, Amsterdam, 1994.

    Google Scholar 

  28. A. Nogin. Quotient types: A modular approach. In V. A. Carreno, C. A. Munoz, and S. Tahar, editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), volume 2410 of Lecture Notes in Computer Science, pages 263–280. Springer-Verlag, 2002. Available at http://nogin.org/papers/quotients.html.

  29. F. Pfenning and C. Schürmann. Twelf — a meta-logical framework for deductive systems. In Ganzinger [Ganzinger, 1999], pages 202206.

    Google Scholar 

  30. R. Pollack. Dependently typed records for representing mathematical structure. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 461–478. Springer-Verlag, 2000.

    Google Scholar 

  31. D. Prawitz. Natural Deduction. Almquist and Wiksell, Stockholm, 1965.

    MATH  Google Scholar 

  32. D. Scott. Constructive validity. In D. L. M. Laudelt, editor, Symposium on Automatic Demonstration, volume 5(3) of Lecture Notes in Mathematics, pages 237–275. Springer-Verlag, New York, 1970.

    Chapter  Google Scholar 

  33. W. W. Tait. Intensional interpretation of functionals of finite type. Journal of Symbolic Logic, 32 (2): 189–212, 1967.

    Article  MathSciNet  Google Scholar 

  34. F. Wiedijk. A contemporary implementation of Automath. Talk presented at the Workshop on 35 years of Automath, Heriot-Watt University, Edinburgh, Scotland, April 10–13, 2002.

    Google Scholar 

  35. J. Zucker. Formalization of classical mathematics in Automath. In Colloque International de Logique, pages 135–145, Paris, 1977. Colloques Internationaux du Centre National de la Recherche Scientifique, CNRS.

    Google Scholar 

Download references

Authors
  1. Robert L. Constable
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Mathematical and Computer Sciences, Heriot-Watt University, Mountbatten Building, EH 14 4AS, Riccarton, Edinburgh, Scotland, UK

    Fairouz D. Kamareddine

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Constable, R.L. (2003). Recent Results in Type Theory and Their Relationship to Automath. In: Kamareddine, F.D. (eds) Thirty Five Years of Automating Mathematics. Applied Logic Series, vol 28. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0253-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-94-017-0253-9_3

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-6440-0

  • Online ISBN: 978-94-017-0253-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation