Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Types for Proofs and Programs

TYPES 1995: Types for Proofs and Programs pp 231–248Cite as

Context-relative syntactic categories and the formalization of mathematical text

  • Conference paper
  • First Online:

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

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, pages 381–392, 1972. Reprinted in R. Nederpelt, editor, Selected Papers on Automath, pages 375–388. North-Holland, Amsterdam, 1994.

    Google Scholar 

  • N.G. de Bruijn. The mathematical vernacular, a language for mathematics with typed sets. R. Nederpelt, editor, Selected Papers on Automath, pages 865–935. North-Holland, Amsterdam, 1994.

    Google Scholar 

  • Yann Coscoy, Gilles Kahn and Laurent Théry. Extracting text from proofs. Rapport de recherche n.2459, INRIA, Sophia-Antipolis, 1995.

    Google Scholar 

  • Lena Magnusson and Bengt Nordström. The ALF Proof Editor and Its Proof Engine. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, pages 213–237. Lecture Notes in Computer Science 806, Springer-Verlag, Heidelberg, 1994.

    Google Scholar 

  • Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984.

    Google Scholar 

  • Richard Montague. Formal Philosophy. Yale University Press, New Haven, 1974. Collected papers edited by Richmond Thomason.

    Google Scholar 

  • Aarne Ranta. Type Theoretical Grammar. Oxford University Press, Oxford, 1994.

    Google Scholar 

  • Aarne Ranta. Syntactic categories in the language of mathematics. In P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proofs and Programs, pages 162–182, Lecture Notes in Computer Science 996, Springer-Verlag, Heidelberg, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Philosophy, University of Helsinki, P.O.Box 24, 00014, Finland

    Aarne Ranta

Authors
  1. Aarne Ranta
    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

Ranta, A. (1996). Context-relative syntactic categories and the formalization of mathematical text. 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_73

Download citation

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

  • 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