{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T05:21:47Z","timestamp":1750742507886},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540403326"},{"type":"electronic","value":"9783540449041"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44904-3_8","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T05:49:32Z","timestamp":1193550572000},"page":"105-119","source":"Crossref","is-referenced-by-count":12,"title":["A Logical Framework with Dependently Typed Records"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Randy","family":"Pollack","sequence":"additional","affiliation":[]},{"given":"Makoto","family":"Takeyama","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"8_CR1","unstructured":"Stuart Allen. A Non-Type-Theoretic Semantics For Type-Theoretic Language. PhD thesis, Cornell Univ., 1987. Report TR87-866."},{"key":"8_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Computer Science Logic, CSL\u201994","author":"D. Aspinall","year":"1995","unstructured":"David Aspinall. Subtyping with singleton types. In Proc. Computer Science Logic, CSL\u201994, volume 933 of LNCS, 1995."},{"issue":"1","key":"8_CR3","first-page":"239","volume":"34","author":"L. Augustsson","year":"1999","unstructured":"Lennart Augustsson. Cayenne \u2014 a language with dependent types. In ICFP\u2019 98, volume 34(1) of SIGPLAN Notices, pages 239\u2013250. ACM, June 1999.","journal-title":"ICFP\u2019 98"},{"key":"8_CR4","unstructured":"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."},{"key":"8_CR5","unstructured":"G. Betarte. Dependent Record Types and Formal Abstract Reasoning. PhD thesis, Chalmers Univ. of Technology, 1998."},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"G. Betarte and A. Tasistro. Extension of Martin-L\u00f6f\u2019s 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.","DOI":"10.1007\/BFb0097801"},{"key":"8_CR7","unstructured":"Coq. The Coq Project, 2002. http:\/\/coq.inria.fr\/ ."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. An algorithm for testing conversion in type theory. In G. Huet and G.D. Plotkin, editors, Logical Frameworks. Cambridge Univ. Press, 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"key":"8_CR9","unstructured":"J. Courant. MC: A module calculus for Pure Type Systems. Technical Report 1217, CNRS Universit\u00e9 Paris Sud 8623: LRI, June 1999."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Judica\u00ebl 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.","DOI":"10.1016\/S1571-0661(04)80490-0"},{"issue":"3","key":"8_CR11","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1017\/S096012950100336X","volume":"11","author":"J.-Y. Girard","year":"2001","unstructured":"Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301\u2013506, 2001.","journal-title":"Mathematical Structures in Computer Science"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In POPL\u201994. ACM Press, 1994.","DOI":"10.1145\/174675.176927"},{"key":"8_CR13","unstructured":"Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. (Submitted for publication.), October 2001."},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1006\/inco.1994.1016","volume":"109","author":"S. Hayashi","year":"1994","unstructured":"S. Hayashi. Singleton, union and intersection types for program extraction. Information and Computation, 109:174\u2013210, 1994.","journal-title":"Information and Computation"},{"key":"8_CR15","unstructured":"Alexei Kopylov. Dependent intersection: A new way of defining records in type theory. Technical Report TR2000-1809, Cornell University, 2000."},{"key":"8_CR16","unstructured":"LEGO. The LEGO Proof Assistant, 2001. www.dcs.ed.ac.uk\/home\/lego\/."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"X. Leroy. Manifest types, modules, and separate compilation. In POPL\u201994, New York, NY, USA, 1994. ACM Press.","DOI":"10.1145\/174675.176926"},{"issue":"5","key":"8_CR18","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1017\/S0956796800001933","volume":"6","author":"X. Leroy","year":"1996","unstructured":"X. Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6(5):667\u2013698, September 1996.","journal-title":"Journal of Functional Programming"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford Univ. Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"D. MacQueen. Using dependent types to express modular structure. In POPL\u201986, 1986.","DOI":"10.1145\/512644.512670"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"J. McKinna and R. Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3\u20134), November 1999.","DOI":"10.1023\/A:1006294005493"},{"key":"8_CR22","series-title":"Lect Notes Comput Sci","volume-title":"5th Conf. on Typed Lambda Calculi and Applications, TLCA\u201901","author":"A. Miquel","year":"2001","unstructured":"Alexandre Miquel. The implicit calculus of constructions. In S. Abramsky, editor, 5th Conf. on Typed Lambda Calculi and Applications, TLCA\u201901, volume 2044 of LNCS. Springer-Verlag, 2001."},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. Smith. Martin-l\u00f6f\u2019s type theory. In Abramsky, Gabbai, and Maibaum, editors, Handbook of Logic in Computer Science, volume 5. Oxford Univ. Press, 2001.","DOI":"10.1093\/oso\/9780198537816.003.0004"},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/s001650200018","volume":"13","author":"R. Pollack","year":"2002","unstructured":"Robert Pollack. Dependently typed records in type theory. Formal Aspects of Computing, 13:386\u2013402, 2002.","journal-title":"Formal Aspects of Computing"},{"key":"8_CR25","unstructured":"Christopher Stone. Singleton Kinds and Singleton Types. PhD thesis, Carnegie Mellon University, 2000. Report CMU-CS-00-153."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44904-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,18]],"date-time":"2024-02-18T18:54:45Z","timestamp":1708282485000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44904-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540403326","9783540449041"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-44904-3_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}