{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:19Z","timestamp":1781238919881,"version":"3.54.1"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171834","type":"print"},{"value":"9783030171841","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17184-1_2","type":"book-chapter","created":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T17:34:04Z","timestamp":1554572044000},"page":"30-59","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Meta-F $$^\\star $$ : Proof Automation with SMT, Tactics, and Metaprograms"],"prefix":"10.1007","author":[{"given":"Guido","family":"Mart\u00ednez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Danel","family":"Ahman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor","family":"Dumitrescu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nick","family":"Giannarakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chris","family":"Hawblitzel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Monal","family":"Narasimhamurthy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zoe","family":"Paraskevopoulou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cl\u00e9ment","family":"Pit-Claudel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,4,6]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Ahman, D., et al.: Dijkstra monads for free. In: POPL (2017). \n                      https:\/\/doi.org\/10.1145\/3009837.3009878","DOI":"10.1145\/3009837.3009878"},{"issue":"POPL","key":"2_CR2","first-page":"65:1","volume":"2","author":"D Ahman","year":"2018","unstructured":"Ahman, D., Fournet, C., Hri\u0163cu, C., Maillard, K., Rastogi, A., Swamy, N.: Recalling a witness: foundations and applications of monotonic state. PACMPL 2(POPL), 65:1\u201365:30 (2018). \n                      https:\/\/arxiv.org\/abs\/1707.02466","journal-title":"PACMPL"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-94821-8_2","volume-title":"Interactive Theorem Proving","author":"A Anand","year":"2018","unstructured":"Anand, A., Boulier, S., Cohen, C., Sozeau, M., Tabareau, N.: Towards certified meta-programming with typed Template-Coq. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 20\u201339. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-94821-8_2\n                      \n                    . \n                      https:\/\/template-coq.github.io\/template-coq\/"},{"key":"2_CR4","unstructured":"Appel, A.W.: Tactics for separation logic. Early Draft (2006). \n                      https:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf"},{"issue":"4","key":"2_CR5","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1093\/logcom\/14.4.447","volume":"14","author":"S Awodey","year":"2004","unstructured":"Awodey, S., Bauer, A.: Propositions as [Types]. J. Log. Comput. 14(4), 447\u2013471 (2004). \n                      https:\/\/doi.org\/10.1093\/logcom\/14.4.447","journal-title":"J. Log. Comput."},{"key":"2_CR6","unstructured":"Barendregt, H., Geuvers, H.: Proof-assistants using dependent type systems. In: Handbook of Automated Reasoning, pp. 1149\u20131238. Elsevier Science Publishers B. V., Amsterdam (2001). \n                      http:\/\/dl.acm.org\/citation.cfm?id=778522.778527"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-69149-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M Barnett","year":"2008","unstructured":"Barnett, M., et al.: The Spec# programming system: challenges and directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 144\u2013152. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-69149-5_16"},{"key":"2_CR9","unstructured":"Barras, B., Gr\u00e9goire, B., Mahboubi, A., Th\u00e9ry, L.: Chap. 25: The ring and field tactic families. Coq reference manual. \n                      https:\/\/coq.inria.fr\/refman\/ring.html"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed lambda-calculus. In: LICS (1991). \n                      https:\/\/doi.org\/10.1109\/LICS.1991.151645","DOI":"10.1109\/LICS.1991.151645"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/11502760_3","volume-title":"Fast Software Encryption","author":"DJ Bernstein","year":"2005","unstructured":"Bernstein, D.J.: The Poly1305-AES message-authentication code. In: Gilbert, H., Handschuh, H. (eds.) FSE 2005. LNCS, vol. 3557, pp. 32\u201349. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11502760_3\n                      \n                    . \n                      https:\/\/cr.yp.to\/mac\/poly1305-20050329.pdf"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F Besson","year":"2007","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48\u201362. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74464-1_4"},{"key":"2_CR13","unstructured":"Bhargavan, K., et al.: Everest: towards a verified, drop-in replacement of HTTPS. In: SNAPL (2017). \n                      http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2017\/7119\/pdf\/LIPIcs-SNAPL-2017-1.pdf"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-40885-4_17","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 245\u2013260. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-40885-4_17"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. JAR 51(1), 109\u2013128 (2013). \n                      https:\/\/doi.org\/10.1007\/s10817-013-9278-5","journal-title":"JAR"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-25379-9_26","volume-title":"Certified Programs and Proofs","author":"M Boespflug","year":"2011","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full reduction at full throttle. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 362\u2013377. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-25379-9_26"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14"},{"key":"2_CR18","unstructured":"Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: USENIX Security (2017). \n                      https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"issue":"3","key":"2_CR19","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. STTT 7(3), 212\u2013232 (2005). \n                      https:\/\/doi.org\/10.1007\/s10009-004-0167-4","journal-title":"STTT"},{"issue":"1","key":"2_CR20","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10817-008-9101-x","volume":"41","author":"A Chaieb","year":"2008","unstructured":"Chaieb, A., Nipkow, T.: Proof synthesis and reflection for linear arithmetic. J. Autom. Reason. 41(1), 33\u201359 (2008). \n                      https:\/\/doi.org\/10.1007\/s10817-008-9101-x","journal-title":"J. Autom. Reason."},{"issue":"3","key":"2_CR21","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). \n                      https:\/\/doi.org\/10.1007\/s10817-011-9225-2","journal-title":"J. Autom. Reason."},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Christiansen, D.R., Brady, E.: Elaborator reflection: extending Idris in Idris. In: ICFP (2016). \n                      https:\/\/doi.org\/10.1145\/2951913.2951932","DOI":"10.1145\/2951913.2951932"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-14295-6_42","volume-title":"Computer Aided Verification","author":"E Cohen","year":"2010","unstructured":"Cohen, E., Moskal, M., Schulte, W., Tobies, S.: Local verification of global invariants in concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 480\u2013494. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-14295-6_42"},{"issue":"3","key":"2_CR24","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10990-007-9015-z","volume":"20","author":"P Cr\u00e9gut","year":"2007","unstructured":"Cr\u00e9gut, P.: Strongly reducing variants of the Krivine abstract machine. HOSC 20(3), 209\u2013230 (2007). \n                      https:\/\/doi.org\/10.1007\/s10990-007-9015-z","journal-title":"HOSC"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"issue":"1\u20134","key":"2_CR26","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"\u0141 Czajka","year":"2018","unstructured":"Czajka, \u0141., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. JAR 61(1\u20134), 423\u2013453 (2018). \n                      https:\/\/doi.org\/10.1007\/s10817-018-9458-4","journal-title":"JAR"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36675-8_2","volume-title":"Automated Reasoning and Mathematics","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 15\u201344. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-36675-8_2\n                      \n                    . \n                      http:\/\/dl.acm.org\/citation.cfm?id=2554473.2554475"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"2_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNAI, vol. 1955, pp. 85\u201395. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/3-540-44404-1_7"},{"issue":"ICFP","key":"2_CR30","doi-asserted-by":"publisher","first-page":"34:1","DOI":"10.1145\/3110278","volume":"1","author":"G Ebner","year":"2017","unstructured":"Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. PACMPL 1(ICFP), 34:1\u201334:29 (2017). \n                      https:\/\/doi.org\/10.1145\/3110278","journal-title":"PACMPL"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-63390-9_7","volume-title":"Computer Aided Verification","author":"B Ekici","year":"2017","unstructured":"Ekici, B., et al.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017, Part II. LNCS, vol. 10427, pp. 126\u2013133. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: IEEE S&P (2019). \n                      https:\/\/doi.org\/10.1109\/SP.2019.00005","DOI":"10.1109\/SP.2019.00005"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8\n                      \n                    . \n                      https:\/\/hal.inria.fr\/hal-00789533\/document"},{"issue":"4S","key":"2_CR34","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2502508.2502520","volume":"48","author":"C Flanagan","year":"2013","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: PLDI 2002: extended static checking for Java. SIGPLAN Not. 48(4S), 22\u201333 (2013). \n                      https:\/\/doi.org\/10.1145\/2502508.2502520","journal-title":"SIGPLAN Not."},{"key":"2_CR35","unstructured":"Fromherz, A., Giannarakis, N., Hawblitzel, C., Parno, B., Rastogi, A., Swamy, N.: A verified, efficient embedding of a verifiable assembly language. PACMPL (POPL) (2019). \n                      https:\/\/github.com\/project-everest\/project-everest.github.io\/raw\/master\/assets\/vale-popl.pdf"},{"issue":"11","key":"2_CR36","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2014the four-color theorem. Not. AMS 55(11), 1382\u20131393 (2008). \n                      https:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf","journal-title":"Not. AMS"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"MJ Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979). \n                      https:\/\/doi.org\/10.1007\/3-540-09724-4"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98\u2013113. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11541868_7"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-662-49674-9_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Grov","year":"2016","unstructured":"Grov, G., Tumas, V.: Tactics for the Dafny program verifier. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 36\u201353. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_3"},{"key":"2_CR40","unstructured":"Hawblitzel, C., et al.: Ironclad apps: end-to-end security via automated full-system verification. In: OSDI (2014). \n                      https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"issue":"7","key":"2_CR41","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/3068608","volume":"60","author":"C Hawblitzel","year":"2017","unstructured":"Hawblitzel, C., et al.: Ironfleet: proving safety and liveness of practical distributed systems. CACM 60(7), 83\u201392 (2017). \n                      https:\/\/doi.org\/10.1145\/3068608","journal-title":"CACM"},{"issue":"ICFP","key":"2_CR42","doi-asserted-by":"publisher","first-page":"78:1","DOI":"10.1145\/3236773","volume":"2","author":"J Kaiser","year":"2018","unstructured":"Kaiser, J., Ziliani, B., Krebbers, R., R\u00e9gis-Gianas, Y., Dreyer, D.: Mtac2: typed tactics for backward reasoning in Coq. PACMPL 2(ICFP), 78:1\u201378:31 (2018). \n                      https:\/\/doi.org\/10.1145\/3236773","journal-title":"PACMPL"},{"issue":"2","key":"2_CR43","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. JAR 53(2), 173\u2013213 (2014). \n                      https:\/\/doi.org\/10.1007\/s10817-014-9303-3","journal-title":"JAR"},{"issue":"3","key":"2_CR44","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. JAR 55(3), 245\u2013256 (2015). \n                      https:\/\/doi.org\/10.1007\/s10817-015-9330-8","journal-title":"JAR"},{"key":"2_CR45","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL (2017). \n                      http:\/\/dl.acm.org\/citation.cfm?id=3009855"},{"issue":"3","key":"2_CR46","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10990-007-9018-9","volume":"20","author":"J-L Krivine","year":"2007","unstructured":"Krivine, J.-L.: A call-by-name lambda-calculus machine. Higher Order Symbol. Comput. 20(3), 199\u2013207 (2007). \n                      https:\/\/doi.org\/10.1007\/s10990-007-9018-9","journal-title":"Higher Order Symbol. Comput."},{"key":"2_CR47","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20\n                      \n                    . \n                      http:\/\/dl.acm.org\/citation.cfm?id=1939141.1939161"},{"key":"2_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/BFb0026441","volume-title":"Compiler Construction","author":"K Rustan","year":"1998","unstructured":"Rustan, K., Leino, M., Nelson, G.: An extended static checker for modula-3. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 302\u2013305. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/BFb0026441"},{"key":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-03359-9_24","volume-title":"Theorem Proving in Higher Order Logics","author":"A McCreight","year":"2009","unstructured":"McCreight, A.: Practical tactics for separation logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 343\u2013358. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-03359-9_24"},{"key":"2_CR50","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-94205-6_13","volume-title":"Automated Reasoning","author":"G Melquiond","year":"2018","unstructured":"Melquiond, G., Rieu-Helft, R.: A Why3 framework for reflection proofs and its application to GMP\u2019s algorithms. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 178\u2013193. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-94205-6_13"},{"issue":"5\u20136","key":"2_CR51","first-page":"865","volume":"18","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, J.G., Birkedal, L.: Hoare type theory, polymorphism and separation. JFP 18(5\u20136), 865\u2013911 (2008). \n                      http:\/\/ynot.cs.harvard.edu\/papers\/jfpsep07.pdf","journal-title":"JFP"},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Nanevski, A., Vafeiadis, V., Berdine, J.: Structuring the verification of heap-manipulating programs. In: POPL (2010). \n                      https:\/\/doi.org\/10.1145\/1706299.1706331","DOI":"10.1145\/1706299.1706331"},{"key":"2_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-45685-6_18","volume-title":"Theorem Proving in Higher Order Logics","author":"A Nogin","year":"2002","unstructured":"Nogin, A.: Quotient types: a modular approach. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 263\u2013280. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45685-6_18"},{"key":"2_CR54","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL (2010). \n                      https:\/\/www21.in.tum.de\/~blanchet\/iwil2010-sledgehammer.pdf"},{"issue":"ICFP","key":"2_CR55","doi-asserted-by":"publisher","first-page":"17:1","DOI":"10.1145\/3110261","volume":"1","author":"J Protzenko","year":"2017","unstructured":"Protzenko, J., et al.: Verified low-level programming embedded in F*. PACMPL 1(ICFP), 17:1\u201317:29 (2017). \n                      https:\/\/doi.org\/10.1145\/3110261","journal-title":"PACMPL"},{"key":"2_CR56","doi-asserted-by":"publisher","unstructured":"Stampoulis, A., Shao, Z.: VeriML: typed computation of logical terms inside a language with effects. In: ICFP (2010). \n                      https:\/\/doi.org\/10.1145\/1863543.1863591","DOI":"10.1145\/1863543.1863591"},{"key":"2_CR57","doi-asserted-by":"crossref","unstructured":"Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. In: PLDI (2013). \n                      https:\/\/www.microsoft.com\/en-us\/research\/publication\/verifying-higher-order-programs-with-the-dijkstra-monad\/","DOI":"10.1145\/2491956.2491978"},{"key":"2_CR58","unstructured":"Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: POPL (2016). \n                      https:\/\/www.fstar-lang.org\/papers\/mumon\/"},{"key":"2_CR59","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton Jones, S.L.: Refinement types for Haskell. In: ICFP (2014). \n                      https:\/\/goto.ucsd.edu\/~nvazou\/refinement_types_for_haskell.pdf"},{"issue":"POPL","key":"2_CR60","doi-asserted-by":"publisher","first-page":"53:1","DOI":"10.1145\/3158141","volume":"2","author":"N Vazou","year":"2018","unstructured":"Vazou, N., et al.: Refinement reflection: complete verification with SMT. PACMPL 2(POPL), 53:1\u201353:31 (2018). \n                      https:\/\/doi.org\/10.1145\/3158141","journal-title":"PACMPL"},{"key":"2_CR61","unstructured":"Wadler, P.: Views: a way for pattern matching to cohabit with data abstraction. In: POPL (1987). \n                      https:\/\/dl.acm.org\/citation.cfm?doid=41625.41653"},{"key":"2_CR62","unstructured":"Wenzel, M.: The Isabelle\/Isar reference manual (2017). \n                      http:\/\/isabelle.in.tum.de\/doc\/isar-ref.pdf"},{"key":"2_CR63","doi-asserted-by":"publisher","unstructured":"Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. JFP 25 (2015). \n                      https:\/\/doi.org\/10.1017\/S0956796815000118","DOI":"10.1017\/S0956796815000118"},{"key":"2_CR64","unstructured":"Zinzindohou\u00e9, J.-K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: CCS (2017). \n                      http:\/\/eprint.iacr.org\/2017\/536"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17184-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:21:35Z","timestamp":1558344095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17184-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171834","9783030171841"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17184-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"6 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"86","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}