{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,24]],"date-time":"2023-08-24T04:17:01Z","timestamp":1692850621813},"reference-count":83,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2017,5,22]],"date-time":"2017-05-22T00:00:00Z","timestamp":1495411200000},"content-version":"unspecified","delay-in-days":21,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2017,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem of searching for errors in such formalizations has attracted comparatively little attention. In this article, we present \u03b1Check, a bounded model checker for metatheoretic properties of formal systems specified using nominal logic. In contrast to the current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the case that a flaw is detected. We present two implementations of this technique, one based on<jats:italic>negation-as-failure<\/jats:italic>and one based on<jats:italic>negation elimination<\/jats:italic>, along with experimental results showing that these techniques are fast enough to be used interactively to debug systems as they are developed.<\/jats:p>","DOI":"10.1017\/s1471068417000035","type":"journal-article","created":{"date-parts":[[2017,5,22]],"date-time":"2017-05-22T11:38:59Z","timestamp":1495453139000},"page":"311-352","source":"Crossref","is-referenced-by-count":4,"title":["\u03b1Check: A mechanized metatheory model checker"],"prefix":"10.1017","volume":"17","author":[{"given":"JAMES","family":"CHENEY","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ALBERTO","family":"MOMIGLIANO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2017,5,22]]},"reference":[{"key":"S1471068417000035_ref78","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"},{"key":"S1471068417000035_ref70","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.027"},{"key":"S1471068417000035_ref80","doi-asserted-by":"crossref","unstructured":"Walker D. , Mackey L. , Ligatti J. , Reis G. A. and August D. I. 2006. Static typing for a faulty lambda calculus. In ICFP '06: Proc. of the 11th ACM SIGPLAN International Conference on Functional Programming. ACM Press, New York, NY, USA, 38\u201349.","DOI":"10.1145\/1159803.1159809"},{"key":"S1471068417000035_ref81","doi-asserted-by":"crossref","unstructured":"Weirich S. , Yorgey B. A. and Sheard T. 2011. Binders unbound. In Proc. of the 16th ACM SIGPLAN International Conference on Functional Programming. ICFP '11. ACM, New York, NY, USA, 333\u2013345.","DOI":"10.1145\/2034773.2034818"},{"key":"S1471068417000035_ref74","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1048"},{"key":"S1471068417000035_ref75","doi-asserted-by":"publisher","DOI":"10.1145\/1656242.1656248"},{"key":"S1471068417000035_ref71","doi-asserted-by":"crossref","unstructured":"Schroeder-Heister P. 1993. Definitional reflection and the completion. In Proc. of the 4th International Workshop on Extensions of Logic Programming (ELP'93), R. Dyckhoff , Ed. Lecture Notes in Computer Science, vol. 798. Springer, St. Andrews, UK, 333\u2013347.","DOI":"10.1007\/3-540-58025-5_65"},{"key":"S1471068417000035_ref64","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"S1471068417000035_ref63","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/2893582.2893594","article-title":"Nominal techniques","volume":"3","author":"Pitts","year":"2016","journal-title":"ACM SIGLOG News"},{"key":"S1471068417000035_ref62","volume-title":"Software Foundations","author":"Pierce","year":"2016"},{"key":"S1471068417000035_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9218-1"},{"key":"S1471068417000035_ref65","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"S1471068417000035_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675"},{"key":"S1471068417000035_ref7","first-page":"12","volume-title":"FroCoS","author":"Blanchette","year":"2011"},{"key":"S1471068417000035_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2159531.2159532"},{"key":"S1471068417000035_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"S1471068417000035_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/937555.937559"},{"key":"S1471068417000035_ref53","first-page":"124","volume-title":"PADL 2000","author":"Moreno-Navarro","year":"2000"},{"key":"S1471068417000035_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"S1471068417000035_ref59","doi-asserted-by":"crossref","unstructured":"Paraskevopoulou Z. , Hritcu C. , D\u00e9n\u00e8s M. , Lampropoulos L. and Pierce B. C. 2015. Foundational property-based testing. In Proc. of the 6th International Conference on Interactive Theorem Proving (ITP 2015), vol. 9236, C. Urban and X. Zhang , Eds. Lecture Notes in Computer Science, Springer, 325\u2013343.","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"S1471068417000035_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"S1471068417000035_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90007-4"},{"key":"S1471068417000035_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.012"},{"key":"S1471068417000035_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2004.07.002"},{"key":"S1471068417000035_ref11","first-page":"92","volume-title":"CPP","author":"Bulwahn","year":"2012"},{"key":"S1471068417000035_ref23","volume-title":"Model Checking","author":"Clarke","year":"2000"},{"key":"S1471068417000035_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8749-3"},{"key":"S1471068417000035_ref20","unstructured":"Cheney J. , Momigliano A. and Pessina M. 2016. Advances in property-based testing for \u03b1Prolog. In Proc. of the 10th International Conference on Tests and Proofs (TAP 2016), B. K. Aichernig and C. A. Furia , Eds. Lecture Notes in Computer Science, vol. 9762. Springer, Vienna, Austria, 37\u201356."},{"key":"S1471068417000035_ref72","first-page":"79","volume-title":"TPHOLs","author":"Sch\u00fcrmann","year":"2009"},{"key":"S1471068417000035_ref12","first-page":"153","volume-title":"LPAR","author":"Bulwahn","year":"2012"},{"key":"S1471068417000035_ref16","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1140641176"},{"key":"S1471068417000035_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-013-9091-1"},{"key":"S1471068417000035_ref10","doi-asserted-by":"crossref","unstructured":"Bruscoli P. , Levi F. , Levi G. and Meo M. C. 1994. Compilative constructive negation in constraint logic programs. In Proc. Trees in Algebra and Programming - CAAP'94, 19th International Colloquium, S. Tison , Ed. Lecture Notes in Computer Science, Springer, vol. 787. 52\u201376.","DOI":"10.1007\/BFb0017473"},{"key":"S1471068417000035_ref3","unstructured":"Ayala-Rinc\u00f3n M. , Fern\u00e1ndez M. and Nantes-Sobrinho D. 2016. Nominal narrowing. In Proc. of 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22\u201326, 2016, Porto, Portugal, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 11:1\u201311:17."},{"key":"S1471068417000035_ref4","first-page":"50","volume-title":"TPHOLs","author":"Aydemir","year":"2005"},{"key":"S1471068417000035_ref69","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"S1471068417000035_ref50","doi-asserted-by":"crossref","unstructured":"Momigliano A. 2012. A supposedly fun thing I may have to do again: A HOAS encoding of Howe's method. In Proc. of the 7th International Workshop on Logical Frameworks and Meta-languages, Theory and Practice. LFMTP '12. ACM, New York, NY, USA, 33\u201342.","DOI":"10.1145\/2364406.2364411"},{"key":"S1471068417000035_ref73","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"S1471068417000035_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/1631687.1596559"},{"key":"S1471068417000035_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.05.012"},{"key":"S1471068417000035_ref77","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:14)2012"},{"key":"S1471068417000035_ref38","doi-asserted-by":"crossref","unstructured":"Heath Q. and Miller D. 2015. A framework for proof certificates in finite state exploration. In Proc. 4th Workshop on Proof eXchange for Theorem Proving, PxTP 2015, C. Kaliszyk and A. Paskevich , Eds. EPTCS, vol. 186. 11\u201326. Open Publishing Association, Berlin, Germany.","DOI":"10.4204\/EPTCS.186.4"},{"key":"S1471068417000035_ref5","first-page":"391","volume-title":"CADE","author":"Baelde","year":"2007"},{"key":"S1471068417000035_ref55","first-page":"3","article-title":"A declarative debugging scheme","volume":"1997","author":"Naish","year":"1997","journal-title":"Journal of Functional and Logic Programming"},{"key":"S1471068417000035_ref54","first-page":"39","volume-title":"FLOPS","author":"Mu\u00f1oz-Hern\u00e1ndez","year":"2004"},{"key":"S1471068417000035_ref22","doi-asserted-by":"crossref","unstructured":"Claessen K. and Hughes J. 2000. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proc. of the 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP 2000). ACM, Montreal, Canada, 268\u2013279.","DOI":"10.1145\/351240.351266"},{"key":"S1471068417000035_ref57","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics - With Isabelle\/HOL","author":"Nipkow","year":"2014"},{"key":"S1471068417000035_ref25","volume-title":"Semantics Engineering with PLT Redex","author":"Felleisen","year":"2009"},{"key":"S1471068417000035_ref18","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu024"},{"key":"S1471068417000035_ref56","first-page":"15","volume-title":"JELIA","author":"Niemel\u00e4","year":"2006"},{"key":"S1471068417000035_ref67","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1145\/1449764.1449803","volume-title":"OOPSLA","author":"Roberson","year":"2008"},{"key":"S1471068417000035_ref66","first-page":"576","volume-title":"CAV 2000","author":"Ramakrishnan","year":"2000"},{"key":"S1471068417000035_ref31","doi-asserted-by":"crossref","unstructured":"Gabbay M. J. and Cheney J. 2004. A sequent calculus for nominal logic. In Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004). IEEE Computer Society, Turku, Finland, 139\u2013148.","DOI":"10.1109\/LICS.2004.1319608"},{"key":"#cr-split#-S1471068417000035_ref58.1","unstructured":"12. Owre S. 2006. Random testing in PVS. In Workshop on Automated Formal Methods"},{"key":"#cr-split#-S1471068417000035_ref58.2","unstructured":"13. (AFM). Informatl proceedings, available at http:\/\/fm.csl.sri.com\/AFM06\/ [Accessed on 25\/04\/2017]."},{"key":"S1471068417000035_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90024-8"},{"key":"S1471068417000035_ref47","unstructured":"Mancarella P. and Pedreschi D. 1988. An algebra of logic programs. In Proc. of the 5th International Conference and Symposium on Logic Programming, R. A. Kowalski and K. A. Bowen , Eds. ALP, IEEE, The MIT Press, Seatle, 1006\u20131023."},{"key":"S1471068417000035_ref39","doi-asserted-by":"crossref","unstructured":"Klein C. , Clements J. , Dimoulas C. , Eastlund C. , Felleisen M. , Flatt M. , McCarthy J. A. , Rafkind J. , Tobin-Hochstadt S. and Findler R. B. 2012a. Run your research: On the effectiveness of lightweight mechanization. In Proc. of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL '12. ACM, New York, NY, USA, 285\u2013296.","DOI":"10.1145\/2103656.2103691"},{"key":"S1471068417000035_ref76","doi-asserted-by":"publisher","DOI":"10.1145\/1877714.1877721"},{"key":"S1471068417000035_ref79","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"S1471068417000035_ref27","doi-asserted-by":"crossref","unstructured":"Fetscher B. , Claessen K. , Palka M. H. , Hughes J. and Findler R. B. 2015. Making random judgments: Automatically generating well-typed terms from the definition of a type-system. In Proc. of ESOP 2015, vol. 9032, J. Vitek , Ed. Lecture Notes in Computer Science, Springer, 383\u2013405.","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"S1471068417000035_ref68","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"S1471068417000035_ref9","first-page":"58","article-title":"Nominal computation theory (Dagstuhl Seminar 13422)","volume":"3","author":"Boja\u0144czyk","year":"2013","journal-title":"Dagstuhl Reports"},{"key":"S1471068417000035_ref1","first-page":"1","volume-title":"Functional and Logic Programming","author":"Amaral","year":"2014"},{"key":"S1471068417000035_ref8","first-page":"131","volume-title":"ITP 2010","author":"Blanchette","year":"2010"},{"key":"S1471068417000035_ref15","unstructured":"Cheney J. 2005b. Scrap your nameplate (functional pearl). In Proc. of the 10th International Conference on Functional Programming (ICFP 2005), B. Pierce , Ed. ACM, Tallinn, Estonia, 180\u2013191."},{"key":"S1471068417000035_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243794"},{"key":"S1471068417000035_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273931"},{"key":"S1471068417000035_ref33","first-page":"177","volume-title":"PPDP","author":"Gacek","year":"2010"},{"key":"S1471068417000035_ref52","unstructured":"Montanari U. and Pistore M. 2005. History-dependent automata: An introduction. In Advanced Lectures of the 5th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-Moby 2005), M. Bernardo and A. Bogliolo , Ed., vol. 3465 of LNCS, Springer, 1\u201328."},{"key":"S1471068417000035_ref30","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1305810911"},{"key":"S1471068417000035_ref61","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S1471068417000035_ref28","unstructured":"Findler R. B. , Klein C. and Fetscher B. 2015. Redex: Practical semantics engineering. URL: http:\/\/docs.racket-lang.org\/redex. [Accessed on 25\/04\/2017]"},{"key":"S1471068417000035_ref82","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"Winskel","year":"1993"},{"key":"S1471068417000035_ref14","unstructured":"Cheney J. 2005a. Relating nominal and higher-order pattern unification. In Proc. of the 19th International Workshop on Unification (UNIF 2005), L. Vigneron , Ed., LORIA Research Report A05-R-022, 104\u2013119."},{"key":"S1471068417000035_ref60","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-6534-3"},{"key":"S1471068417000035_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9164-3"},{"key":"S1471068417000035_ref26","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1145\/1069774.1069779","volume-title":"PPDP","author":"Fern\u00e1ndez","year":"2005"},{"key":"S1471068417000035_ref43","first-page":"409","article-title":"Constraint logic programming with hereditary Harrop formulas","volume":"1","author":"Leach","year":"2001","journal-title":"TPLP"},{"key":"S1471068417000035_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(90)90023-X"},{"key":"S1471068417000035_ref41","doi-asserted-by":"crossref","unstructured":"Lakin M. R. and Pitts A. M. 2009. Resolving inductive definitions with binders in higher-order typed functional programming. In Proc. the 18th European Symposium on Programming (ESOP 2009), Springer, York, UK, 47\u201361.","DOI":"10.1007\/978-3-642-00590-9_4"},{"key":"S1471068417000035_ref44","unstructured":"Levy J. and Villaret M. 2010. An efficient nominal unification algorithm. In Proc. of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, Springer, Edinburgh, Scottland, UK, 209\u2013226."},{"key":"S1471068417000035_ref49","first-page":"411","volume-title":"CSL","author":"Momigliano","year":"2000"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068417000035","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,23]],"date-time":"2023-08-23T17:38:05Z","timestamp":1692812285000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068417000035\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5]]},"references-count":83,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["S1471068417000035"],"URL":"https:\/\/doi.org\/10.1017\/s1471068417000035","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5]]}}}