{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T05:21:43Z","timestamp":1741238503431,"version":"3.38.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,5,17]],"date-time":"2011-05-17T00:00:00Z","timestamp":1305590400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,10]]},"DOI":"10.1007\/s10817-011-9228-z","type":"journal-article","created":{"date-parts":[[2011,5,16]],"date-time":"2011-05-16T09:07:57Z","timestamp":1305536877000},"page":"427-451","source":"Crossref","is-referenced-by-count":2,"title":["Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover"],"prefix":"10.1007","volume":"49","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wilmer","family":"Ricciotti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,5,17]]},"reference":[{"issue":"1","key":"9228_CR1","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s12046-009-0003-3","volume":"34","author":"A Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: A compact kernel for the calculus of inductive constructions. Sadhana 34(1), 71\u2013144 (2009)","journal-title":"Sadhana"},{"key":"9228_CR2","unstructured":"Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: Crafting a proof assistant. In: Proceedings of Types 2006: Conference of the Types Project (2006)"},{"issue":"2","key":"9228_CR3","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A Asperti","year":"2007","unstructured":"Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. J. Autom. Reason. (Special Issue on User Interfaces for Theorem Proving) 39(2), 109\u2013139 (2007)","journal-title":"J. Autom. Reason."},{"key":"9228_CR4","doi-asserted-by":"crossref","unstructured":"Aydemir, B., Bohannon, A., Fairbairn, M., Foster, J., Pierce, B., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: the POPLmark challenge. In: Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005) (2005)","DOI":"10.1007\/11541868_4"},{"key":"9228_CR5","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 3\u201315 (2008)","DOI":"10.1145\/1328438.1328443"},{"key":"9228_CR6","first-page":"750","volume-title":"Proc. of 1st Int. Symp. on Theor. Aspects of Computer Software, TACS\u201991, Sendai, Japan, 24\u201327 Sept 1991, vol. 526 of Lecture Notes in Computer Science","author":"L Cardelli","year":"1991","unstructured":"Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of system F with subtyping (TACS). In: Ito, T., Meyer, A.R. (eds.) Proc. of 1st Int. Symp. on Theor. Aspects of Computer Software, TACS\u201991, Sendai, Japan, 24\u201327 Sept 1991, vol. 526 of Lecture Notes in Computer Science, pp. 750\u2013770. Springer, Berlin (1991)"},{"key":"9228_CR7","unstructured":"Chargu\u00e9raud, A.: Submissions to the PoplMark Challenge. http:\/\/www.chargueraud.orgarthur\/research\/2006\/poplmark\/ (2006)"},{"key":"9228_CR8","unstructured":"Chlipala, A.: Submission to the PoplMark Challenge. http:\/\/adam.chlipala.net\/poplmark\/ (2006)"},{"key":"9228_CR9","unstructured":"Coq: The Coq Proof Assistant Reference Manual, Version 8.0. The Coq Development Team (2004)"},{"key":"9228_CR10","doi-asserted-by":"crossref","unstructured":"Cornes, C., Terrasse, D.: Automating inversion of inductive predicates in Coq\u2019. In: TYPES \u201995: Selected Papers from the International Workshop on Types for Proofs and Programs, pp. 85\u2013104. London, UK (1996)","DOI":"10.1007\/3-540-61780-9_64"},{"key":"9228_CR11","doi-asserted-by":"crossref","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax involving binders. In: 14th Annual Symposium on Logic in Computer Science, pp. 214\u2013224. Washington, DC, USA (1999)","DOI":"10.1109\/LICS.1999.782617"},{"key":"9228_CR12","unstructured":"Guidi, F.: Lambda Types on the Lambda Calculus with Abbreviations. Research report UBLCS-2006-25, Department of Computer Science, University of Bologna (2006)"},{"key":"9228_CR13","unstructured":"Hirschowitz, A., Maggesi, M.: Submission to the PoplMark Challenge. http:\/\/web.math.unifi.it\/~maggesi\/poplmark\/Part1a.v (2007)"},{"key":"9228_CR14","unstructured":"Leroy, X.: A Locally Nameless Solution to the POPLmark Challenge. Research report 6098, INRIA (2007)"},{"key":"9228_CR15","unstructured":"McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) Types for Proofs and Programs (Proceedings of the International Workshop, TYPES\u201900), vol. 2277 of LNCS (2002)"},{"issue":"2","key":"9228_CR16","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"AM Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic: a first order theory of names and binding. Inf. Comput. 186(2), 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"key":"9228_CR17","first-page":"313","volume-title":"Proceedings of the Workshop on Types for Proofs and Programs","author":"R Pollack","year":"1993","unstructured":"Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T. (eds.) Proceedings of the Workshop on Types for Proofs and Programs, pp.\u00a0313\u2013332. Nijmegen, The Netherlands (1993)"},{"key":"9228_CR18","unstructured":"Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: Tinycals: step by step tacticals. In: Proceedings of User Interface for Theorem Provers 2006 (2006)"},{"key":"9228_CR19","unstructured":"Sallinens, J.: Submission to the PoplMark Challenge. https:\/\/alliance.seas.upenn.edu\/\u223cplclub\/cgibin\/poplmark\/index.php?title=Submission_by_Jevgenijs_Sallinens (2007)"},{"key":"9228_CR20","unstructured":"Stump, A.: Submission to the PoplMark Challenge. http:\/\/www.cs.uiowa.edu\/~astump\/poplmark-coq\/ (2005)"},{"key":"9228_CR21","unstructured":"Urban, C., Pollack, R.: Strong induction principles in the locally nameless representation of binders. In: Workshop on Mechanized Metatheory (2007)"},{"key":"9228_CR22","unstructured":"Vouillon, J.: Submission to the PoplMark Challenge. http:\/\/www.cis.upenn.edu\/~plclub\/wiki-static\/vouillon-coq\/part-a.v (2005)"},{"key":"9228_CR23","unstructured":"Werner, B.: Une Th\u00e9orie des Constructions Inductives. Ph.D. thesis, Universit\u00e9 Paris VII (1994)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9228-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9228-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9228-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T15:06:43Z","timestamp":1741187203000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9228-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,17]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["9228"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9228-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2011,5,17]]}}}