{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:12:34Z","timestamp":1767928354864,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705932","type":"print"},{"value":"9783540705949","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70594-9_4","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"29-56","source":"Crossref","is-referenced-by-count":18,"title":["Verifying a Semantic \u03b2\u03b7-Conversion Test for Martin-L\u00f6f Type Theory"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Dybjer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_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)"},{"issue":"4","key":"4_CR2","first-page":"345","volume":"77","author":"A. Abel","year":"2005","unstructured":"Abel, A., Coquand, T.: Untyped algorithmic equality for Martin-L\u00f6f\u2019s logical framework with surjective pairs. Fundam. Inform.\u00a077(4), 345\u2013395 (2005); TLCA 2005 special issue","journal-title":"Fundam. Inform."},{"key":"4_CR3","unstructured":"Altenkirch, T., Chapman, J.: Big step normalisation. Draft, available on the authors\u2019 homepages (2008)"},{"key":"4_CR4","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":"4_CR5","unstructured":"Abel, A., Coquand, T., Dybjer, P.: A semantic \u03b2\u03b7-equality algorithm for Martin-L\u00f6f Type Theory (extended version). Technical report, Ludwig-Maximilians-University Munich (2008), http:\/\/www.tcs.ifi.lmu.de\/~abel\/semEqTR.pdf"},{"key":"4_CR6","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0304-3975(84)90123-3","volume":"31","author":"K.B. Bruce","year":"1984","unstructured":"Bruce, K.B., Longo, G.: On combinatory algebras and their expansions. Theor. Comput. Sci.\u00a031, 31\u201340 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed \u03bb-calculus. In: Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pp. 203\u2013211 (July 1991)","DOI":"10.1109\/LICS.1991.151645"},{"key":"4_CR9","unstructured":"Chapman, J., Altenkirch, T., McBride, C.: Epigram reloaded: a standalone typechecker for ETT. In: van Eekelen, M.C.J.D. (ed.) Revised Selected Papers from the 6th Symp. on Trends in Functional Programming, TFP 2005, Trends in Functional Programming, Intellect, vol.\u00a06, pp. 79\u201394 (2007)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BFb0049326","volume-title":"Proc. of the 7th Wksh. on Computer Science Logic, CSL 1993","author":"C. Coquand","year":"1994","unstructured":"Coquand, C.: From semantics to rules: A machine assisted analysis. In: Meinke, K., B\u00f6rger, E., Gurevich, Y. (eds.) Proc. of the 7th Wksh. on Computer Science Logic, CSL 1993. LNCS, vol.\u00a0832, pp. 91\u2013105. Springer, Heidelberg (1994)"},{"key":"4_CR11","series-title":"Science of Computer Programming","first-page":"167","volume-title":"Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction","author":"T. Coquand","year":"1996","unstructured":"Coquand, T.: An algorithm for type-checking dependent types. In: Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction, Kloster Irsee, Germany, July 17\u201321, 1995. Science of Computer Programming, vol.\u00a026, pp. 167\u2013177. Elsevier Science, Amsterdam (1996)"},{"issue":"1-2","key":"4_CR12","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(1-2), 113\u2013134 (2005)","journal-title":"Fundam. Inform."},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/3-540-47018-2_16","volume-title":"Partial Evaluation \u2013 Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark","author":"O. Danvy","year":"1999","unstructured":"Danvy, O.: Type-directed partial evaluation. In: Hatcliff, J., Mogensen, T.\u00c6., Thiemann, P. (eds.) Partial Evaluation \u2013 Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998. LNCS, vol.\u00a01706, pp. 367\u2013411. Springer, Heidelberg (1999)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/3-540-61780-9_66","volume-title":"Types for Proofs and Programs (TYPES 1995)","author":"P. Dybjer","year":"1996","unstructured":"Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) Types for Proofs and Programs (TYPES 1995). LNCS, vol.\u00a01158, pp. 120\u2013134. Springer, Heidelberg (1996)"},{"issue":"2","key":"4_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(2), 525\u2013549 (2000)","journal-title":"The Journal of Symbolic Logic"},{"key":"4_CR16","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/581478.581501","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":"4_CR17","unstructured":"H. Goguen.: A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh. Available as LFCS Report ECS-LFCS-94-304 (August 1994)"},{"issue":"1","key":"4_CR18","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/1042038.1042041","volume":"6","author":"R. Harper","year":"2005","unstructured":"Harper, R., Pfenning, F.: On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic\u00a06(1), 61\u2013101 (2005)","journal-title":"ACM Transactions on Computational Logic"},{"key":"4_CR19","unstructured":"INRIA. The Coq Proof Assistant, Version 8.1. INRIA (2007), http:\/\/coq.inria.fr\/"},{"key":"4_CR20","first-page":"42","volume-title":"Proc. of the 33rd ACM Symp. on Principles of Programming Languages, POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proc. of the 33rd ACM Symp. on Principles of Programming Languages, POPL 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: About models for intuitionistic type theories and the notion of definitional equality. In: Kanger, S. (ed.) Proceedings of the 3rd Scandinavian Logic Symposium, pp. 81\u2013109 (1975)","DOI":"10.1016\/S0049-237X(08)70727-4"},{"key":"4_CR22","unstructured":"P. Martin-L\u00f6f.: Substitution calculus. Lecture in G\u00f6teborg (November 1992) (unpublished)"},{"key":"4_CR23","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-41296 G\u00f6teborg, Sweden (September 2007)"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1145\/1147954.1147961","volume":"53","author":"A.M. Pitts","year":"2006","unstructured":"Pitts, A.M.: Alpha-structural recursion and induction. Journal of the ACM\u00a053, 459\u2013506 (2006)","journal-title":"Journal of the ACM"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3-540-58085-9_82","volume-title":"Types for Proofs and Programs: International Workshop","author":"R. Pollack","year":"1994","unstructured":"Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T. (eds.) Types for Proofs and Programs: International Workshop. LNCS, vol.\u00a0806, pp. 313\u2013332. Springer, Heidelberg (1994)"},{"key":"4_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE-16)","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction (CADE-16). LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Pierce, B.C., Turner, D.N.: Local type inference. In: POPL 98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California (1998)","DOI":"10.1145\/268946.268967"},{"key":"4_CR28","unstructured":"Shinwell, M.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, University of Cambridge (2005)"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, C., Sarnat, J.: Structural logical relations. In: Pfenning, F. (ed.) Proc. of the 23nd IEEE Symp. on Logic in Computer Science (LICS 2008) (2008)","DOI":"10.1109\/LICS.2008.44"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70594-9_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:08:31Z","timestamp":1605762511000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70594-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705932","9783540705949"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70594-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}