Skip to main content
SpringerLink
Log in

A Logical Framework with Dependently Typed Records

  • Conference paper
  • First Online:
Typed Lambda Calculi and Applications (TLCA 2003)

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

Included in the following conference series:

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. Stuart Allen. A Non-Type-Theoretic Semantics For Type-Theoretic Language. PhD thesis, Cornell Univ., 1987. Report TR87-866.

    Google Scholar 

  2. David Aspinall. Subtyping with singleton types. In Proc. Computer Science Logic, CSL’94, volume 933 of LNCS, 1995.

    Google Scholar 

  3. Lennart Augustsson. Cayenne — a language with dependent types. In ICFP’ 98, volume 34(1) of SIGPLAN Notices, pages 239–250. ACM, June 1999.

    Google Scholar 

  4. H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.

    Google Scholar 

  5. G. Betarte. Dependent Record Types and Formal Abstract Reasoning. PhD thesis, Chalmers Univ. of Technology, 1998.

    Google Scholar 

  6. G. Betarte and A. Tasistro. Extension of Martin-Löf’s type theory with record types and subtyping. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998.

    Google Scholar 

  7. Coq. The Coq Project, 2002. http://coq.inria.fr/.

  8. Thierry Coquand. An algorithm for testing conversion in type theory. In G. Huet and G.D. Plotkin, editors, Logical Frameworks. Cambridge Univ. Press, 1991.

    Google Scholar 

  9. J. Courant. MC: A module calculus for Pure Type Systems. Technical Report 1217, CNRS Université Paris Sud 8623: LRI, June 1999.

    Google Scholar 

  10. Judicaël Courant. Strong normalization with singleton types. In Stefan Van Bakel, editor, Second Workshop on Intersection Types and Related Systems, volume 70 of Electronic Notes in Computer Science. Elsevier, 2002.

    Google Scholar 

  11. Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301–506, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  12. R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL’94. ACM Press, 1994.

    Google Scholar 

  13. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. (Submitted for publication.), October 2001.

    Google Scholar 

  14. S. Hayashi. Singleton, union and intersection types for program extraction. Information and Computation, 109:174–210, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  15. Alexei Kopylov. Dependent intersection: A new way of defining records in type theory. Technical Report TR2000-1809, Cornell University, 2000.

    Google Scholar 

  16. LEGO. The LEGO Proof Assistant, 2001. www.dcs.ed.ac.uk/home/lego/.

    Google Scholar 

  17. X. Leroy. Manifest types, modules, and separate compilation. In POPL’94, New York, NY, USA, 1994. ACM Press.

    Google Scholar 

  18. X. Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6(5):667–698, September 1996.

    Article  MATH  MathSciNet  Google Scholar 

  19. Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford Univ. Press, 1994.

    Google Scholar 

  20. D. MacQueen. Using dependent types to express modular structure. In POPL’86, 1986.

    Google Scholar 

  21. J. McKinna and R. Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3–4), November 1999.

    Google Scholar 

  22. Alexandre Miquel. The implicit calculus of constructions. In S. Abramsky, editor, 5th Conf. on Typed Lambda Calculi and Applications, TLCA’01, volume 2044 of LNCS. Springer-Verlag, 2001.

    Google Scholar 

  23. B. Nordström, K. Petersson, and J. Smith. Martin-löf’s type theory. In Abramsky, Gabbai, and Maibaum, editors, Handbook of Logic in Computer Science, volume 5. Oxford Univ. Press, 2001.

    Google Scholar 

  24. Robert Pollack. Dependently typed records in type theory. Formal Aspects of Computing, 13:386–402, 2002.

    Article  MATH  Google Scholar 

  25. Christopher Stone. Singleton Kinds and Singleton Types. PhD thesis, Carnegie Mellon University, 2000. Report CMU-CS-00-153.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Chalmers Tekniska Högskola, Sweden

    Thierry Coquand & Makoto Takeyama

  2. Edinburgh University, UK

    Randy Pollack

Authors
  1. Thierry Coquand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Randy Pollack
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Makoto Takeyama
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

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

    Martin Hofmann

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coquand, T., Pollack, R., Takeyama, M. (2003). A Logical Framework with Dependently Typed Records. In: Hofmann, M. (eds) Typed Lambda Calculi and Applications. TLCA 2003. Lecture Notes in Computer Science, vol 2701. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44904-3_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-44904-3_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-44904-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation