{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:07:43Z","timestamp":1725484063197},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540432876"},{"type":"electronic","value":"9783540458425"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_4","type":"book-chapter","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T20:00:38Z","timestamp":1180209638000},"page":"53-62","source":"Crossref","is-referenced-by-count":1,"title":["An Implementation of Type:Type"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Makoto","family":"Takeyama","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Augustsson, L. Cayenne, A language with dependent types. in Proceedings of ICFP\u201998, ACM Press, 1998, 239\u2013250.","DOI":"10.1145\/289423.289451"},{"issue":"1\u20133","key":"4_CR2","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/S0019-9958(83)80033-3","volume":"59","author":"H. Barendregt","year":"1983","unstructured":"Barendregt, H. and Rezus, A. Semantics for classical AUTOMATH and related systems. Inform. and Control 59 (1983), no. 1\u20133, 127\u2013147.","journal-title":"Inform. and Control"},{"key":"4_CR3","unstructured":"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"},{"key":"4_CR4","unstructured":"Cardelli, L. A polymorphic lambda-calculus with Type:Type. SRC Research Report 10, Digital Equipment Corporation Systems Research Center, May 1, 1986."},{"key":"4_CR5","first-page":"73","volume-title":"Twenty-five years of constructive type theory (Venice, 1995)","author":"C. Coquand","year":"1998","unstructured":"Coquand, C. A realizability interpretation of Martin-L\u00f6f\u2019s type theory. Twenty-five years of constructive type theory (Venice, 1995), 73\u201382, Oxford Logic Guides, 36, Oxford Univ. Press, New York, 1998."},{"issue":"1\u20133","key":"4_CR6","first-page":"167","volume":"26","author":"Th. Coquand","year":"1996","unstructured":"Coquand, Th. An algorithm for type-checking dependent types. Mathematics of program construction (Kloster Irsee, 1995). Sci. Comput. Programming 26 (1996), no. 1\u20133, 167\u2013177.","journal-title":"Mathematics of program construction (Kloster Irsee, 1995). Sci. Comput. Programming"},{"key":"4_CR7","unstructured":"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."},{"key":"4_CR8","series-title":"Lect Notes Comput Sci","first-page":"19","volume-title":"Types for Proofs and Programs","author":"L.S. Jutting","year":"1993","unstructured":"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\u201361."},{"issue":"3","key":"4_CR9","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R. A theory of type polymorphism in programming. J. Comput. System Sci. 17 (1978), no. 3, 348\u2013375.","journal-title":"J. Comput. System Sci."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013292.","DOI":"10.1007\/978-94-009-7893-5_9"},{"key":"4_CR11","unstructured":"van Daalen, D. The language theory of Automath, PhD thesis, Eindhoven, 1980."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45842-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:03:04Z","timestamp":1556434984000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}