{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T09:09:37Z","timestamp":1781341777193,"version":"3.54.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100006112","name":"Microsoft Research","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100006112","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/K034413\/1"],"award-info":[{"award-number":["EP\/K034413\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1618756, CNS-1518765, CCF-1518844, CCF-1422471, CCF-1223850, and CCF-1218344"],"award-info":[{"award-number":["CCF-1618756, CNS-1518765, CCF-1518844, CCF-1422471, CCF-1223850, and CCF-1218344"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>\n            We introduce\n            <jats:italic>Refinement Reflection<\/jats:italic>\n            , a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function\u2019s (output) refinement type. As a consequence, at\n            <jats:italic>uses<\/jats:italic>\n            of the function, the function definition is instantiated in the SMT logic in a precise fashion that permits decidable verification. Reflection allows the user to write\n            <jats:italic>equational proofs<\/jats:italic>\n            of programs just by writing other programs using pattern-matching and recursion to perform case-splitting and induction. Thus, via the propositions-as-types principle, we show that reflection permits the\n            <jats:italic>specification<\/jats:italic>\n            of arbitrary functional correctness properties. Finally, we introduce a proof-search algorithm called\n            <jats:italic>Proof by Logical Evaluation<\/jats:italic>\n            that uses techniques from model checking and abstract interpretation, to completely automate equational reasoning. We have implemented reflection in Liquid Haskell and used it to verify that the widely used instances of the Monoid, Applicative, Functor, and Monad typeclasses actually satisfy key algebraic laws required to make the clients safe, and have used reflection to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism.\n          <\/jats:p>","DOI":"10.1145\/3158141","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":47,"title":["Refinement reflection: complete verification with SMT"],"prefix":"10.1145","volume":"2","author":[{"given":"Niki","family":"Vazou","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anish","family":"Tondwalkar","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vikraman","family":"Choudhury","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ryan G.","family":"Scott","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ryan R.","family":"Newton","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philip","family":"Wadler","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK \/ Input Output HK, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"N. Amin K. R. M. L. and T. Rompf. 2014. Computing with an SMT Solver. In TAP.  N. Amin K. R. M. L. and T. Rompf. 2014. Computing with an SMT Solver. In TAP.","DOI":"10.1007\/978-3-319-09099-3_2"},{"key":"e_1_2_2_2_1","unstructured":"A. Appel. 2016. Verified Functional Algorithms. https:\/\/www.cs.princeton.edu\/~appel\/vfa\/Perm.html .  A. Appel. 2016. Verified Functional Algorithms. https:\/\/www.cs.princeton.edu\/~appel\/vfa\/Perm.html ."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2678015.2682546"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"L. Augustsson. 1998. Cayenne - a Language with Dependent Types.. In ICFP.  L. Augustsson. 1998. Cayenne - a Language with Dependent Types.. In ICFP.","DOI":"10.1145\/289423.289451"},{"key":"e_1_2_2_5_1","unstructured":"C. Barrett A. Stump and C. Tinelli. 2010. The SMT-LIB Standard: Version 2.0.  C. Barrett A. Stump and C. Tinelli. 2010. The SMT-LIB Standard: Version 2.0."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.27"},{"key":"e_1_2_2_7_1","unstructured":"Y. Bertot and P. Cast\u00e9ran. 2004. Coq\u2019Art: The Calculus of Inductive Constructions. Springer Verlag.  Y. Bertot and P. Cast\u00e9ran. 2004. Coq\u2019Art: The Calculus of Inductive Constructions. Springer Verlag."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/32.2.122"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"e_1_2_2_10_1","unstructured":"Jr. Bocchino L. Robert V. S. Adve S. V. Adve and M. Snir. 2009. Parallel Programming Must Be Deterministic by Default. In HotPar .  Jr. Bocchino L. Robert V. S. Adve S. V. Adve and M. Snir. 2009. Parallel Programming Must Be Deterministic by Default. In HotPar ."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806643"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143235"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_35"},{"key":"e_1_2_2_16_1","unstructured":"R. L. Constable and S. F. Smith. 1987. Partial Objects In Constructive Type Theory. In LICS.  R. L. Constable and S. F. Smith. 1987. Partial Objects In Constructive Type Theory. In LICS."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra. 1975. Guarded Commands Nondeterminacy and Formal Derivation of Programs. In Communications of the ACM .  E. W. Dijkstra. 1975. Guarded Commands Nondeterminacy and Formal Derivation of Programs. In Communications of the ACM .","DOI":"10.1145\/800027.808417"},{"key":"e_1_2_2_19_1","volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","unstructured":"E. W. Dijkstra . 1976. A Discipline of Programming . Prentice-Hall . E. W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633361"},{"key":"e_1_2_2_21_1","volume-title":"HERMIT: Tool Support for Equational Reasoning on GHC Core Programs. In Haskell.","author":"Farmer A.","year":"2015","unstructured":"A. Farmer , N. Sculthorpe , and A. Gill . 2015 . Reasoning with the HERMIT: Tool Support for Equational Reasoning on GHC Core Programs. In Haskell. A. Farmer, N. Sculthorpe, and A. Gill. 2015. Reasoning with the HERMIT: Tool Support for Equational Reasoning on GHC Core Programs. In Haskell."},{"key":"e_1_2_2_22_1","unstructured":"G. Gentzen. 1935. Inverstigations into Logical Deduction. In American Philosophical Quarterly.  G. Gentzen. 1935. Inverstigations into Logical Deduction. In American Philosophical Quarterly."},{"key":"e_1_2_2_23_1","unstructured":"W. A. Howard. 1980. The formulae-as-types notion of construction. In Essays on Combinatory Logic Lambda Calculus and Formalism .  W. A. Howard. 1980. The formulae-as-types notion of construction. In Essays on Combinatory Logic Lambda Calculus and Formalism ."},{"key":"e_1_2_2_24_1","volume-title":"A tutorial on the universality and expressiveness of fold. J. Functional Programming","author":"Hutton G.","year":"1999","unstructured":"G. Hutton . 1999. A tutorial on the universality and expressiveness of fold. J. Functional Programming ( 1999 ). G. Hutton. 1999. A tutorial on the universality and expressiveness of fold. J. Functional Programming (1999)."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908091"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535842"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"K. R. M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR.  K. R. M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR.","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"e_1_2_2_30_1","unstructured":"K. R. M. Leino and N. Polikarpova. 2016. Verified Calculations. In VSTTE.  K. R. M. Leino and N. Polikarpova. 2016. Verified Calculations. In VSTTE."},{"key":"e_1_2_2_31_1","volume-title":"https:\/\/github.com\/Microsoft\/dafny\/blob\/master\/Test\/dafny0\/Fuel.dfy","author":"Leino R.","year":"2016","unstructured":"R. Leino . 2016. Dafny. ( 2016 ). https:\/\/github.com\/Microsoft\/dafny\/blob\/master\/Test\/dafny0\/Fuel.dfy . R. Leino. 2016. Dafny. (2016). https:\/\/github.com\/Microsoft\/dafny\/blob\/master\/Test\/dafny0\/Fuel.dfy ."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034685"},{"key":"e_1_2_2_33_1","volume-title":"Agda: Dependent Types for Relational Program Derivation. In J. Funct. Program.","author":"Mu S. C.","year":"2009","unstructured":"S. C. Mu , H. S. Ko , and P. Jansson . 2009 . Algebra of Programming in Agda: Dependent Types for Relational Program Derivation. In J. Funct. Program. S. C. Mu, H. S. Ko, and P. Jansson. 2009. Algebra of Programming in Agda: Dependent Types for Relational Program Derivation. In J. Funct. Program."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"T. Nipkow L.C. Paulson and M. Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic.  T. Nipkow L.C. Paulson and M. Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8141-3_34"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_2_2_42_1","doi-asserted-by":"crossref","unstructured":"J. Rushby S. Owre and N. Shankar. 1998. Subtypes for Specifications: Predicate Subtyping in PVS. TSE.  J. Rushby S. Owre and N. Shankar. 1998. Subtypes for Specifications: Predicate Subtyping in PVS. TSE.","DOI":"10.1109\/32.713327"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676974"},{"key":"e_1_2_2_45_1","volume-title":"Zeno: An Automated Prover for Properties of Recursive Data Structures. In TACAS.","author":"Sonnex W.","year":"2012","unstructured":"W. Sonnex , S. Drossopoulou , and S. Eisenbach . 2012 . Zeno: An Automated Prover for Properties of Recursive Data Structures. In TACAS. W. Sonnex, S. Drossopoulou, and S. Eisenbach. 2012. Zeno: An Automated Prover for Properties of Recursive Data Structures. In TACAS."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","unstructured":"N. Swamy C. Hri\u0163cu C. Keller A. Rastogi A. Delignat-Lavaud S. Forest K. Bhargavan C. Fournet P. Y. Strub M. Kohlweiss J. K. Zinzindohoue and S. Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In POPL.  N. Swamy C. Hri\u0163cu C. Keller A. Rastogi A. Delignat-Lavaud S. Forest K. Bhargavan C. Fournet P. Y. Strub M. Kohlweiss J. K. Zinzindohoue and S. Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In POPL.","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_50_1","unstructured":"G. Tourlakis. 2008. Ackermann\u2019s Function. (2008). http:\/\/www.cs.yorku.ca\/~gt\/papers\/Ackermann-function.pdf .  G. Tourlakis. 2008. Ackermann\u2019s Function. (2008). http:\/\/www.cs.yorku.ca\/~gt\/papers\/Ackermann-function.pdf ."},{"key":"e_1_2_2_51_1","volume":"2017","author":"Vazou N.","unstructured":"N. Vazou , L. Lampropoulos , and J. Polakow. 2017 a. A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq. In Haskell. N. Vazou, L. Lampropoulos, and J. Polakow. 2017a. A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq. In Haskell.","journal-title":"J. Polakow."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_54_1","volume-title":"Extended Version: Refinement Reflection: Complete Verification with SMT.","author":"Vazou N.","year":"2017","unstructured":"N. Vazou , A. Tondwalkar , V. Choudhury , R. G. Scott , R. R. Newton , P. Wadler , and R. Jhala . 2017 b. Extended Version: Refinement Reflection: Complete Verification with SMT. (2017). https:\/\/nikivazou.github.io\/static\/popl18\/ extended-refinement-reflection.pdf N. Vazou, A. Tondwalkar, V. Choudhury, R. G. Scott, R. R. Newton, P. Wadler, and R. Jhala. 2017b. Extended Version: Refinement Reflection: Complete Verification with SMT. (2017). https:\/\/nikivazou.github.io\/static\/popl18\/ extended-refinement-reflection.pdf"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908110"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/24697.24706"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699407"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158141","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158141","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158141","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":57,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158141"],"URL":"https:\/\/doi.org\/10.1145\/3158141","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}