Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Stuart Allen. A Non-Type-Theoretic Semantics For Type-Theoretic Language. PhD thesis, Cornell Univ., 1987. Report TR87-866.
David Aspinall. Subtyping with singleton types. In Proc. Computer Science Logic, CSL’94, volume 933 of LNCS, 1995.
Lennart Augustsson. Cayenne — a language with dependent types. In ICFP’ 98, volume 34(1) of SIGPLAN Notices, pages 239–250. ACM, June 1999.
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.
G. Betarte. Dependent Record Types and Formal Abstract Reasoning. PhD thesis, Chalmers Univ. of Technology, 1998.
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.
Coq. The Coq Project, 2002. http://coq.inria.fr/.
Thierry Coquand. An algorithm for testing conversion in type theory. In G. Huet and G.D. Plotkin, editors, Logical Frameworks. Cambridge Univ. Press, 1991.
J. Courant. MC: A module calculus for Pure Type Systems. Technical Report 1217, CNRS Université Paris Sud 8623: LRI, June 1999.
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.
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.
R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL’94. ACM Press, 1994.
Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. (Submitted for publication.), October 2001.
S. Hayashi. Singleton, union and intersection types for program extraction. Information and Computation, 109:174–210, 1994.
Alexei Kopylov. Dependent intersection: A new way of defining records in type theory. Technical Report TR2000-1809, Cornell University, 2000.
LEGO. The LEGO Proof Assistant, 2001. www.dcs.ed.ac.uk/home/lego/.
X. Leroy. Manifest types, modules, and separate compilation. In POPL’94, New York, NY, USA, 1994. ACM Press.
X. Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6(5):667–698, September 1996.
Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford Univ. Press, 1994.
D. MacQueen. Using dependent types to express modular structure. In POPL’86, 1986.
J. McKinna and R. Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3–4), November 1999.
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.
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.
Robert Pollack. Dependently typed records in type theory. Formal Aspects of Computing, 13:386–402, 2002.
Christopher Stone. Singleton Kinds and Singleton Types. PhD thesis, Carnegie Mellon University, 2000. Report CMU-CS-00-153.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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