{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:30:56Z","timestamp":1784845856210,"version":"3.55.0"},"reference-count":100,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T00:00:00Z","timestamp":1732147200000},"content-version":"unspecified","delay-in-days":20,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2024,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Property-based testing (PBT) is a technique for validating code against an executable specification by automatically generating test-data. We present a proof-theoretical reconstruction of this style of testing for relational specifications and employ the Foundational Proof Certificate framework to describe test generators. We do this by encoding certain kinds of \u201cproof outlines\u201d as proof certificates that can describe various common generation strategies in the PBT literature, ranging from random to exhaustive, including their combination. We also address the <jats:italic>shrinking<\/jats:italic> of counterexamples as a first step toward their explanation. Once generation is accomplished, the testing phase is a standard logic programing search. After illustrating our techniques on simple, first-order (algebraic) data structures, we lift it to data structures containing bindings by using the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1471068424000176_inline1.png\"\/><jats:tex-math>\n$\\lambda$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-tree syntax approach to encode bindings. The <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1471068424000176_inline2.png\"\/><jats:tex-math>\n$\\lambda$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>Prolog programing language can perform both generating and checking of tests using this approach to syntax. We then further extend PBT to specifications in a fragment of linear logic.<\/jats:p>","DOI":"10.1017\/s1471068424000176","type":"journal-article","created":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T12:57:02Z","timestamp":1732193822000},"page":"1123-1162","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Property-Based Testing by Elaborating Proof Outlines"],"prefix":"10.1017","volume":"24","author":[{"given":"DALE","family":"MILLER","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0942-4777","authenticated-orcid":false,"given":"ALBERTO","family":"MOMIGLIANO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2024,11,21]]},"reference":[{"key":"S1471068424000176_ref28","volume-title":"Semantics Engineering with PLT Redex","author":"Felleisen","year":"2009"},{"key":"S1471068424000176_ref87","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"S1471068424000176_ref90","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"S1471068424000176_ref92","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.05.008"},{"key":"S1471068424000176_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000143"},{"key":"S1471068424000176_ref1","unstructured":"Andreoli, J.-M. and Pareschi, R. 1990. Linear objects: Logical processes with built-in inheritance. In Proceeding of the Seventh International Conference on Logic Programming, MIT Press, Jerusalem."},{"key":"S1471068424000176_ref7","first-page":"12","volume-title":"FroCoS","volume":"6989","author":"Blanchette","year":"2011"},{"key":"S1471068424000176_ref75","first-page":"330","article-title":"Induction and co-induction in sequent calculus","volume":"10","author":"Momigliano","year":"2012","journal-title":"Journal of Applied Logic"},{"key":"S1471068424000176_ref61","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00171-1"},{"key":"S1471068424000176_ref19","unstructured":"Chirimar, J. 1995. Proof Theoretic Approach to Specification Languages. Ph.D. thesis, University of Pennsylvania."},{"key":"S1471068424000176_ref21","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S1471068424000176_ref76","first-page":"245","volume-title":"Types in Logic Programming","author":"Nadathur","year":"1992"},{"key":"S1471068424000176_ref77","doi-asserted-by":"crossref","unstructured":"Palka, M. H. , Claessen, K. , Russo, A. and Hughes, J. 2011. Testing an optimising compiler by generating random lambda terms. In A. Bertolino, H. Foster and J. J. Li, Eds. Proceedings of the 6th International Workshop on Automation of Software Test, Waikiki, Honolulu, HI, USA, 91\u201397.","DOI":"10.1145\/1982595.1982615"},{"key":"S1471068424000176_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0103100"},{"key":"S1471068424000176_ref47","doi-asserted-by":"crossref","unstructured":"Hritcu, C. , Hughes, J. , Pierce, B. C. , Spector-Zabusky, A. , Vytiniotis, D. , Azevedo de Amorim, A. and Lampropoulos, L. 2013. Testing noninterference, quickly. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. ICFP\u201913, ACM, New York, NY, USA, 455\u2013468.","DOI":"10.1145\/2500365.2500574"},{"key":"S1471068424000176_ref80","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24754-8_4"},{"key":"S1471068424000176_ref93","first-page":"222","volume-title":"8th Symp. on Logic in Computer Science","author":"Schroeder-Heister","year":"1993"},{"key":"S1471068424000176_ref97","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"S1471068424000176_ref41","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.5.635"},{"key":"S1471068424000176_ref14","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2951"},{"key":"S1471068424000176_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841700045X"},{"key":"S1471068424000176_ref95","unstructured":"Selinger, P. 2008. Lecture notes on the lambda calculus. Available at https:\/\/arxiv.org\/abs\/0804.3434"},{"key":"S1471068424000176_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000666"},{"key":"S1471068424000176_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009868"},{"key":"S1471068424000176_ref35","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1935"},{"key":"S1471068424000176_ref73","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.072"},{"key":"S1471068424000176_ref100","doi-asserted-by":"publisher","DOI":"10.1145\/1656242.1656248"},{"key":"S1471068424000176_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90051-5"},{"key":"S1471068424000176_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9380-6"},{"key":"S1471068424000176_ref24","first-page":"293","volume-title":"Negation as failure","author":"Clark","year":"1978"},{"key":"S1471068424000176_ref53","doi-asserted-by":"publisher","DOI":"10.1145\/3360607"},{"key":"S1471068424000176_ref55","volume-title":"QuickChick: Property-Based Testing in Coq","volume":"4","author":"Lampropoulos","year":"2023"},{"key":"S1471068424000176_ref70","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068421000533"},{"key":"S1471068424000176_ref91","doi-asserted-by":"crossref","unstructured":"Schack-Nielsen, A. and Sch\u00fcrmann, C. 2008. Celf - A logical framework for deductive and concurrent systems (system description). In Lecture Notes in Computer Science, IJCAR, Springer, vol. 5195, 320\u2013326.","DOI":"10.1007\/978-3-540-71070-7_28"},{"key":"S1471068424000176_ref94","unstructured":"Sch\u00fcrmann, C. 2000. Automating the Meta Theory of Deductive Systems. Ph.D. thesis, Carnegie Mellon University. CMU-CS-00-146."},{"key":"S1471068424000176_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S1471068424000176_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"S1471068424000176_ref69","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9483-3"},{"key":"S1471068424000176_ref84","doi-asserted-by":"crossref","unstructured":"Pfenning, F. and Simmons, R. J. 2009. Substructural operational semantics as ordered logic programming. In LICS, IEEE Computer Society, 101\u2013110.","DOI":"10.1109\/LICS.2009.8"},{"key":"S1471068424000176_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9218-1"},{"key":"S1471068424000176_ref74","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"S1471068424000176_ref5","doi-asserted-by":"crossref","unstructured":"Baelde, D. , Gacek, A. , Miller, D. , Nadathur, G. and Tiu, A. 2007. The Bedwyr system for model checking over syntactic expressions. In F. Pfenning, Ed. LNAI, 21th Conf. on Automated Deduction (CADE), Springer, New York, vol. 4603, 391\u2013397.","DOI":"10.1007\/978-3-540-73595-3_28"},{"key":"S1471068424000176_ref81","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2832"},{"key":"S1471068424000176_ref96","doi-asserted-by":"crossref","unstructured":"Sullivan, K. , Yang, J. , Coppit, D. , Khurshid, S. and Jackson, D. 2004. Software assurance by bounded exhaustive testing. In Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA\u201904, ACM, New York, NY, USA, 133\u2013142.","DOI":"10.1145\/1007512.1007531"},{"key":"S1471068424000176_ref85","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_18"},{"key":"S1471068424000176_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"S1471068424000176_ref88","unstructured":"Polakow, J. and Yi, K. 2000. Proving syntactic properties of exceptions in an ordered logical framework. In The First Asian Workshop on Programming Languages and Systems, APLAS 2000, National University of Singapore, Singapore, Proceedings, December 18-20, 2000, 23\u201332."},{"key":"S1471068424000176_ref99","unstructured":"Tassi, E. 2018. Elpi: An extension language for Coq (Metaprogramming Coq in the Elpi Prolog dialect). Working paper or preprint."},{"key":"S1471068424000176_ref86","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"S1471068424000176_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"S1471068424000176_ref31","first-page":"383","volume-title":"ESOP","volume":"9032","author":"Fetscher","year":"2015"},{"key":"S1471068424000176_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000323"},{"key":"S1471068424000176_ref48","doi-asserted-by":"crossref","unstructured":"Hughes, J. 2007. Quickcheck testing for fun and profit. In M. Hanus, Ed. Lecture Notes in Computer Science, Practical Aspects of Declarative Languages, 9th International Symposium, PADL 2007, January 14-15, 2007, Nice, France, 4354, Springer, vol. 1\u201332,","DOI":"10.1007\/978-3-540-69611-7_1"},{"key":"S1471068424000176_ref78","doi-asserted-by":"crossref","unstructured":"Paraskevopoulou, Z. , Eline, A. and Lampropoulos, L. 2022. Computing correctly with inductive relations. In R. Jhala and I. Dillig, Eds. PLDI\u201922: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, ACM, 966\u2013980.","DOI":"10.1145\/3519939.3523707"},{"key":"S1471068424000176_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/BF00244460"},{"key":"S1471068424000176_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364515"},{"key":"S1471068424000176_ref43","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001559"},{"key":"S1471068424000176_ref54","first-page":"45:1","article-title":"Generating good generators for inductive relations","volume":"2","author":"Lampropoulos","year":"2018","journal-title":"Proceedings of the ACM on Programming Languages, POPL"},{"key":"S1471068424000176_ref98","first-page":"110","volume-title":"ICLP Technical Communications. EPTCS","volume":"325","author":"Tarau","year":"2020"},{"key":"S1471068424000176_ref10","volume-title":"Principles and Practice of Programming Languages 2019 (PPDP\u201919)","author":"Blanco","year":"2019"},{"key":"S1471068424000176_ref4","first-page":"1","article-title":"Abella: A system for reasoning about relational specifications","volume":"7","author":"Baelde","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"S1471068424000176_ref46","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"S1471068424000176_ref65","first-page":"15:1","article-title":"Effect-driven quickchecking of compilers","volume":"1","author":"Midtgaard","year":"2017","journal-title":"PACMPL"},{"key":"S1471068424000176_ref82","doi-asserted-by":"crossref","unstructured":"Pfenning, F. and Elliott, C. 1988. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, ACM Press, 199\u2013208.","DOI":"10.1145\/53990.54010"},{"key":"S1471068424000176_ref60","unstructured":"Martin, A. 2010. Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study. Ph.D. thesis, University of Ottawa.https:\/\/ruor.uottawa.ca\/handle\/10393\/19711"},{"key":"S1471068424000176_ref64","volume-title":"Extensions of Logic Programming","author":"Michaylov","year":"1992"},{"key":"S1471068424000176_ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_6"},{"key":"S1471068424000176_ref9","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.197.2"},{"key":"S1471068424000176_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"S1471068424000176_ref38","unstructured":"Girard, J.-Y. 1992. A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu."},{"key":"S1471068424000176_ref8","doi-asserted-by":"crossref","unstructured":"Blanco, R. , Chihani, Z. and Miller, D. 2017. Translating between implicit and explicit versions of proof. In L. de Moura, Ed. Lecture Notes in Computer Science, Automated Deduction - CADE 26 \u2014 26th International Conference on Automated Deduction, Springer, vol. 10395, 255\u2013273.","DOI":"10.1007\/978-3-319-63046-5_16"},{"key":"S1471068424000176_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9475-3"},{"key":"S1471068424000176_ref50","unstructured":"Kahn, G. 1987. Natural semantics. In F.-J. Brandenburg, G. Vidal-Naquet and M. Wirsing, Eds. Proceedings of the Symposium on Theoretical Aspects of Computer Science, Springer, vol. 247, 22\u201339, Lecture Notes in Computer Science."},{"key":"S1471068424000176_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_20"},{"key":"S1471068424000176_ref66","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00045-X"},{"key":"S1471068424000176_ref63","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00168-2"},{"key":"S1471068424000176_ref59","first-page":"92","volume-title":"Logic-Based Program Synthesis and Transformation - 31st International Symposium, LOPSTR 2021, Tallinn, Estonia, September 7-8, 2021, Proceedings","volume":"13290","author":"Mantovani","year":"2021"},{"key":"S1471068424000176_ref89","unstructured":"Qi, X. , Gacek, A. , Holte, S. , Nadathur, G. and Snow, Z. 2015. The Teyjus system \u2013 version 2. Available at http:\/\/teyjus.cs.umn.edu\/."},{"key":"S1471068424000176_ref23","doi-asserted-by":"crossref","unstructured":"Claessen, K. and Hughes, J. 2000. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), ACM, 268\u2013279.","DOI":"10.1145\/357766.351266"},{"key":"S1471068424000176_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014053"},{"key":"S1471068424000176_ref58","first-page":"10:1","volume-title":"26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy","volume":"188","author":"Manighetti","year":"2020"},{"key":"S1471068424000176_ref71","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"key":"S1471068424000176_ref72","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"S1471068424000176_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_10"},{"key":"S1471068424000176_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"S1471068424000176_ref51","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. 2012.Run your research: On the effectiveness of lightweight mechanization. In Proceedings 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":"S1471068424000176_ref57","unstructured":"Manighetti, M. 2022. Developing Proof Theory for Proof Exchange. Ph.D. thesis, Institut Polytechnique de Paris."},{"key":"S1471068424000176_ref11","doi-asserted-by":"crossref","unstructured":"Borras, P. , Cl\u00e9ment, D. , Despeyroux, T. , Incerpi, J. , Kahn, G. , Lang, B. and Pascual, V. 1988. Centaur: The system. In Third Annual Symposium on Software Development Environments (SDE3), ACM, Boston, 14\u201324.","DOI":"10.1145\/64137.65005"},{"key":"S1471068424000176_ref68","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0393-z"},{"key":"S1471068424000176_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41135-4_3"},{"key":"S1471068424000176_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S1471068424000176_ref56","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09527-x"},{"key":"S1471068424000176_ref25","doi-asserted-by":"crossref","unstructured":"de Barrio, L. E. B. , Fredlund, L. , Herranz, \u00c1. , Earle, C. B. and Mari no, J. 2021. Makina: A new Quickcheck state machine library. In S. Aronis and A. Bieniusa, Eds. Proceedings of the 20th ACM SIGPLAN International Workshop on Erlang, Erlang@ICFP 2021, Virtual Event, August 26, 2021, Korea, 41\u201353.","DOI":"10.1145\/3471871.3472964"},{"key":"S1471068424000176_ref62","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504080"},{"key":"S1471068424000176_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/322326.322339"},{"key":"S1471068424000176_ref79","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"S1471068424000176_ref83","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"S1471068424000176_ref20","doi-asserted-by":"crossref","unstructured":"Chlipala, A. 2008. Parametric higher-order abstract syntax for mechanized semantics. In J. Hook and P. Thiemann, Eds. Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, September 20-28, 2008, Victoria, BC, Canada, ACM, 143\u2013156.","DOI":"10.1145\/1411203.1411226"},{"key":"S1471068424000176_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068417000035"},{"key":"S1471068424000176_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"}],"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\/S1471068424000176","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T02:03:01Z","timestamp":1736992981000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068424000176\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11]]},"references-count":100,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,11]]}},"alternative-id":["S1471068424000176"],"URL":"https:\/\/doi.org\/10.1017\/s1471068424000176","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}