{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T02:11:40Z","timestamp":1725847900667},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319294728"},{"type":"electronic","value":"9783319294735"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-29473-5_8","type":"book-chapter","created":{"date-parts":[[2016,1,23]],"date-time":"2016-01-23T07:58:11Z","timestamp":1453535891000},"page":"127-141","source":"Crossref","is-referenced-by-count":4,"title":["A Mechanized Textbook Proof of a Type Unification Algorithm"],"prefix":"10.1007","author":[{"given":"Rodrigo","family":"Ribeiro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos","family":"Camar\u00e3o","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,24]]},"reference":[{"key":"8_CR1","volume-title":"Haskell 98 Language and Libraries: The Revised Report","author":"S Peyton Jones","year":"2003","unstructured":"Peyton Jones, S.: Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003)"},{"key":"8_CR2","volume-title":"Definition of Standard ML","author":"R Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: Definition of Standard ML. MIT Press, Cambridge (1990)"},{"issue":"3","key":"8_CR3","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. Syst. Sci. 17(3), 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"8_CR4","first-page":"389","volume-title":"Advanced Topics in Types and Programming Languages","author":"F Pottier","year":"2005","unstructured":"Pottier, F., R\u00e9my, D.: The essence of ML type inference. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, pp. 389\u2013489. MIT Press, Cambridge (2005)"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, New York (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of agda \u2013 a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73\u201378. Springer, Heidelberg (2009)"},{"key":"8_CR8","unstructured":"Paulson, L.C.: Verifying the unification algorithm in lcf. CoRR cs.LO\/9301101 (1993)"},{"key":"8_CR9","unstructured":"Bove, A.: Programming in Martin-L\u00f6f type theory: Unification - A non-trivial example. Licentiate Thesis of the Department of Computer Science, Chalmers University of Technology, November 1999"},{"issue":"6","key":"8_CR10","doi-asserted-by":"publisher","first-page":"1061","DOI":"10.1017\/S0956796803004957","volume":"13","author":"C McBride","year":"2003","unstructured":"McBride, C.: First-order unification by structural recursion. J. Funct. Program. 13(6), 1061\u20131075 (2003)","journal-title":"J. Funct. Program."},{"key":"8_CR11","doi-asserted-by":"crossref","first-page":"24","DOI":"10.4204\/EPTCS.42.3","volume":"42","author":"Sunil Kothari","year":"2010","unstructured":"Kothari, S., Caldwell, J.: A machine checked model of idempotent mgu axioms for lists of equational constraints. In: Fernandez, M. (ed.): Proceedings 24th International Workshop on Unification. EPTCS, vol. 42, pp. 24\u201338 (2010)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"8_CR12","volume-title":"Foundations of Programming Languages","author":"JC Mitchell","year":"1996","unstructured":"Mitchell, J.C.: Foundations of Programming Languages. MIT Press, Cambridge (1996)"},{"key":"8_CR13","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"issue":"1","key":"8_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Program. 14(1), 69\u2013111 (2004)","journal-title":"J. Funct. Program."},{"issue":"7","key":"8_CR15","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/3-540-47813-2_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Barthe","year":"2002","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., de Sousa, S.M.: A formal correspondence between offensive and defensive JavaCard virtual machines. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, p. 32. Springer, Heidelberg (2002)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-87827-8_28","volume-title":"Computer Mathematics","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, pp. 333\u2013333. Springer, Heidelberg (2008)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Engineering mathematics: the odd order theorem proof. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 1\u20132. ACM (2013)","DOI":"10.1145\/2480359.2429071"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Ribeiro, R., et al.: A mechanized textbook proof of a type unification algorithm \u2013 on-line repository (2015). \n                      https:\/\/github.com\/rodrigogribeiro\/unification","DOI":"10.1007\/978-3-319-29473-5_8"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen, M., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, vol. 10. Elsevier (2006)","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"8_CR21","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types","author":"Adam Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"issue":"5","key":"8_CR22","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"N Bruijn de","year":"1972","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings) 75(5), 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae (Proceedings)"},{"issue":"3","key":"8_CR23","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. 49(3), 363\u2013408 (2012)","journal-title":"J. Autom. Reason."},{"key":"8_CR24","unstructured":"Coq Developement Team: Coq Proof Assistant \u2013 Reference Manual (2014). \n                      http:\/\/coq.inria.fr\/distrib\/current\/refman\/\/"},{"key":"8_CR25","unstructured":"Pierce, B.C., Casinghino, C., Gaboardi, M., Greenberg, M., Hri\u0163cu, C., Sjoberg, V., Yorgey, B.: Software Foundations. Electronic textbook (2015)"},{"issue":"3","key":"8_CR26","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/BF01941137","volume":"28","author":"B Nordstr\u00f6m","year":"1988","unstructured":"Nordstr\u00f6m, B.: Terminating general recursion. BIT Numer. Math. 28(3), 605\u2013619 (1988)","journal-title":"BIT Numer. Math."},{"key":"8_CR27","unstructured":"McBride, C.: First-order unification by structural recursion \u2013 correctness proof"},{"issue":"3","key":"8_CR28","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1023\/A:1006277616879","volume":"23","author":"W Naraschewski","year":"1999","unstructured":"Naraschewski, W., Nipkow, T.: Type inference verified: algorithm w in isabelle\/hol. J. Autom. Reason. 23(3), 299\u2013318 (1999)","journal-title":"J. Autom. Reason."},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-13824-9_10","volume-title":"Logic, Language, Information and Computation","author":"AB Avelar","year":"2010","unstructured":"Avelar, A.B., de Moura, F.L.C., Galdino, A.L., Ayala-Rinc\u00f3n, M.: Verification of the completeness of unification algorithms \u00e0 la Robinson. In: Queiroz, R., Dawar, A. (eds.) WoLLIC 2010. LNCS, vol. 6188, pp. 110\u2013124. Springer, Heidelberg (2010)"},{"issue":"5","key":"8_CR30","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1093\/jigpal\/jzu012","volume":"22","author":"AB Avelar","year":"2014","unstructured":"Avelar, A.B., Galdino, A.L., de Moura, F.L.C., Ayala-Rinc\u00f3n, M.: First-order unification in the PVS proof assistant. Logic J. IGPL 22(5), 758\u2013789 (2014)","journal-title":"Logic J. IGPL"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29473-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T11:29:18Z","timestamp":1559388558000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29473-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319294728","9783319294735"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29473-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}