Skip to main content
SpringerLink
Log in

An Implementation of Type:Type

  • Conference paper
  • First Online:
Book cover Types for Proofs and Programs (TYPES 2000)

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

Included in the following conference series:

Abstract

We present a denotational semantics of a type system with dependent types, where types are interpreted as finitary projections. We prove then the correctness of a type-checking algorithm w.r.t. this semantics. In this way, we can justify some simple optimisation in this algorithm. We then sketch how to extend this semantics to allow a simple record mechanism with manifest fields.

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. Augustsson, L. Cayenne, A language with dependent types. in Proceedings of ICFP’98, ACM Press, 1998, 239–250.

    Google Scholar 

  2. Barendregt, H. and Rezus, A. Semantics for classical AUTOMATH and related systems. Inform. and Control 59 (1983), no. 1–3, 127–147.

    Article  MATH  MathSciNet  Google Scholar 

  3. Selected papers on Automath. Edited by R. P. Nederpelt, J. H. Geuvers and R. C. de Vrijer with the assistance of L. S. van Benthem Jutting and D. T. van Daalen. Studies in Logic and the Foundations of Mathematics, 133. North-Holland Publishing Co., Amsterdam, 1994

    Google Scholar 

  4. Cardelli, L. A polymorphic lambda-calculus with Type:Type. SRC Research Report 10, Digital Equipment Corporation Systems Research Center, May 1, 1986.

    Google Scholar 

  5. Coquand, C. A realizability interpretation of Martin-Löf’s type theory. Twenty-five years of constructive type theory (Venice, 1995), 73–82, Oxford Logic Guides, 36, Oxford Univ. Press, New York, 1998.

    Google Scholar 

  6. Coquand, Th. An algorithm for type-checking dependent types. Mathematics of program construction (Kloster Irsee, 1995). Sci. Comput. Programming 26 (1996), no. 1–3, 167–177.

    MATH  MathSciNet  Google Scholar 

  7. Hickey J. Formal Objects in Type Theory Using Very Dependent Types. in Informal proceedings of Third Workshop on Foundations of Object-Oriented Languages (FOOL 3), 1996.

    Google Scholar 

  8. Jutting, L.S. van Benthem, McKinna J. and Pollack R. Checking Algorithms for Pure Type Systems. In Types for Proofs and Programs, LNCS 806, H. Barendregt and T. Nipkow (Eds.) 1993, 19–61.

    Google Scholar 

  9. Milner, R. A theory of type polymorphism in programming. J. Comput. System Sci. 17 (1978), no. 3, 348–375.

    Article  MATH  MathSciNet  Google Scholar 

  10. Scott, D. Lectures on a Mathematical Theory of Computation. in Theoretical foundations of programming methodology. Papers presented at the NATO Summer School, Munich, 1981. Edited by Manfred Broy and Gunther Schmidt. NATO Advanced Study Institute Series C: Mathematical and Physical Sciences, 91. D. Reidel Publishing Co., Dordrecht-Boston, Mass., 1982, 145–292.

    Google Scholar 

  11. van Daalen, D. The language theory of Automath, PhD thesis, Eindhoven, 1980.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, Chalmers University, Sweden

    Thierry Coquand & Makoto Takeyama

  2. Department of Computing Science, Göteborg University, Sweden

    Thierry Coquand & Makoto Takeyama

Authors
  1. Thierry Coquand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Makoto Takeyama
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK

    Paul Callaghan , Zhaohui Luo , James McKinna  & Robert Pollack , ,  & 

  2. Division of Informatics Laboratory for Foundations of Computer Science, The University of Edinburgh, James Clerk Maxwell Building, The King’s Buildings Mayfield Road, EH9 3JZ, Edinburgh, Scotland, UK

    Robert Pollack

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coquand, T., Takeyama, M. (2002). An Implementation of Type:Type. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds) Types for Proofs and Programs. TYPES 2000. Lecture Notes in Computer Science, vol 2277. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45842-5_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-45842-5_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45842-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation