{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:34:30Z","timestamp":1743003270672,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642022722"},{"type":"electronic","value":"9783642022739"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02273-9_3","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T10:12:17Z","timestamp":1246011137000},"page":"5-19","source":"Crossref","is-referenced-by-count":12,"title":["A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]},{"given":"Miguel","family":"Pagano","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Electr. Notes in Theor. Comp. Sci","first-page":"17","volume-title":"Proc. of the 23rd Conf. on the Mathematical Foundations of Programming Semantics (MFPS XXIII)","author":"A. Abel","year":"2007","unstructured":"Abel, A., Aehlig, K., Dybjer, P.: Normalization by evaluation for Martin-L\u00f6f type theory with one universe. In: Fiore, M. (ed.) Proc. of the 23rd Conf. on the Mathematical Foundations of Programming Semantics (MFPS XXIII). Electr. Notes in Theor. Comp. Sci, vol.\u00a0173, pp. 17\u201339. Elsevier, Amsterdam (2007)"},{"key":"3_CR2","first-page":"3","volume-title":"Proc. of the 22nd IEEE Symp. on Logic in Computer Science (LICS 2007)","author":"A. Abel","year":"2007","unstructured":"Abel, A., Coquand, T., Dybjer, P.: Normalization by evaluation for Martin-L\u00f6f Type Theory with typed equality judgements. In: Proc. of the 22nd IEEE Symp. on Logic in Computer Science (LICS 2007), pp. 3\u201312. IEEE Computer Soc. Press, Los Alamitos (2007)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-78969-7_2","volume-title":"Functional and Logic Programming","author":"A. Abel","year":"2008","unstructured":"Abel, A., Coquand, T., Dybjer, P.: On the algebraic foundation of proof assistants for intuitionistic type theory. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol.\u00a04989, pp. 3\u201313. Springer, Heidelberg (2008)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-540-70594-9_4","volume-title":"Mathematics of Program Construction","author":"A. Abel","year":"2008","unstructured":"Abel, A., Coquand, T., Dybjer, P.: Verifying a semantic \u03b2\u03b7-conversion test for Martin-L\u00f6f type theory. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol.\u00a05133, pp. 29\u201356. Springer, Heidelberg (2008)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Abel, A., Coquand, T., Pagano, M.: A modular type-checking algorithm for type theory with singleton types and proof irrelevance (full version) (2009), http:\/\/www.tcs.ifi.lmu.de\/~abel\/singleton.pdf","DOI":"10.1007\/978-3-642-02273-9_3"},{"key":"3_CR6","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"S. Abramsky","year":"1994","unstructured":"Abramsky, S., Jung, A.: Domain Theory. In: Handbook of Logic in Computer Science, pp. 1\u2013168. Oxford University Press, Oxford (1994)"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1017\/S096012950400427X","volume":"14","author":"K. Aehlig","year":"2004","unstructured":"Aehlig, K., Joachimski, F.: Operational aspects of untyped normalization by evaluation. Math. Struct. in Comput. Sci.\u00a014, 587\u2013611 (2004)","journal-title":"Math. Struct. in Comput. Sci."},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0022243","volume-title":"Computer Science Logic","author":"D. Aspinall","year":"1995","unstructured":"Aspinall, D.: Subtyping with singleton types. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, pp. 1\u201315. Springer, Heidelberg (1995)"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1093\/logcom\/14.4.447","volume":"14","author":"S. Awodey","year":"2004","unstructured":"Awodey, S., Bauer, A.: Propositions as [Types]. J. Log. Comput.\u00a014, 447\u2013471 (2004)","journal-title":"J. Log. Comput."},{"key":"3_CR10","first-page":"203","volume-title":"Proc. of the 6th IEEE Symp. on Logic in Computer Science (LICS 1991)","author":"U. Berger","year":"1991","unstructured":"Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed \u03bb-calculus. In: Proc. of the 6th IEEE Symp. on Logic in Computer Science (LICS 1991), pp. 203\u2013211. IEEE Computer Soc. Press, Los Alamitos (1991)"},{"key":"3_CR11","unstructured":"Bruijn, N.G.d.: Some extensions of Automath: the AUT-4 family (1994)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Cartmell, J.: Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32\u2013209 (1986)","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0167-6423(95)00021-6","volume":"26","author":"T. Coquand","year":"1996","unstructured":"Coquand, T.: An algorithm for type-checking dependent types. Science of Computer Programming\u00a026, 167\u2013177 (1996)","journal-title":"Science of Computer Programming"},{"key":"3_CR14","first-page":"113","volume":"65","author":"T. Coquand","year":"2005","unstructured":"Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. Fundam. Inform.\u00a065, 113\u2013134 (2005)","journal-title":"Fundam. Inform."},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"525","DOI":"10.2307\/2586554","volume":"65","author":"P. Dybjer","year":"2000","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic\u00a065, 525\u2013549 (2000)","journal-title":"The Journal of Symbolic Logic"},{"key":"3_CR16","series-title":"SIGPLAN Notices","first-page":"235","volume-title":"Proc. of the 7th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2002)","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proc. of the 7th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2002). SIGPLAN Notices, vol.\u00a037, pp. 235\u2013246. ACM Press, New York (2002)"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. Journal of the Association of Computing Machinery\u00a040, 143\u2013184 (1993)","journal-title":"Journal of the Association of Computing Machinery"},{"key":"3_CR18","unstructured":"INRIA: The Coq Proof Assistant, Version 8.1. INRIA (2007), http:\/\/coq.inria.fr"},{"key":"3_CR19","first-page":"173","volume-title":"Proc. of the 34th ACM Symp. on Principles of Programming Languages, POPL 2007","author":"D.K. Lee","year":"2007","unstructured":"Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: Hofmann, M., Felleisen, M. (eds.) Proc. of the 34th ACM Symp. on Principles of Programming Languages, POPL 2007, pp. 173\u2013184. ACM Press, New York (2007)"},{"key":"3_CR20","unstructured":"Maillard, O.-A.: Proof-irrelevance, strong-normalisation in Type-Theory and PER. Technical report, Chalmers Institute of Technology (2006)"},{"key":"3_CR21","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis (1984)"},{"key":"3_CR22","unstructured":"Martin-L\u00f6f, P.: Normalization by evaluation and by the method of computability, Talk at JAIST. Japan Advanced Institute of Science and Technology, Kanazawa (2004)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/11546382_3","volume-title":"Advanced Functional Programming","author":"C. McBride","year":"2005","unstructured":"McBride, C.: Epigram: Practical programming with dependent types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol.\u00a03622, pp. 130\u2013170. Springer, Heidelberg (2005)"},{"key":"3_CR24","unstructured":"Mitchell, J.C., Moggi, E.: Kripke-Style models for typed lambda calculus. In: LICS, pp. 303\u2013314 (1987)"},{"key":"3_CR25","volume-title":"Programming in Martin L\u00f6f\u2019s Type Theory: An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin L\u00f6f\u2019s Type Theory: An Introduction. Clarendon Press, Oxford (1990)"},{"key":"3_CR26","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, G\u00f6teborg, Sweden (2007)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-44616-3_3","volume-title":"Recent Trends in Algebraic Development Techniques","author":"N. Shankar","year":"2000","unstructured":"Shankar, N., Owre, S.: Principles and Pragmatics of Subtyping in PVS. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 37\u201352. Springer, Heidelberg (2000)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M. Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset coercions in Coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"3_CR29","doi-asserted-by":"publisher","first-page":"676","DOI":"10.1145\/1183278.1183281","volume":"7","author":"C.A. Stone","year":"2006","unstructured":"Stone, C.A., Harper, R.: Extensional equivalence and singleton types. ACM Trans. Comput. Logic\u00a07, 676\u2013722 (2006)","journal-title":"ACM Trans. Comput. Logic"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Werner, B.: On the strength of proof-irrelevant type theories. Logical Meth. in Comput. Sci. 4 (2008)","DOI":"10.2168\/LMCS-4(3:13)2008"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02273-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T23:19:44Z","timestamp":1558394384000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02273-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642022722","9783642022739"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02273-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}