{"id":366,"date":"2021-04-07T06:37:24","date_gmt":"2021-04-07T06:37:24","guid":{"rendered":"http:\/\/easyconferences.eu\/itp2021\/?page_id=366"},"modified":"2021-06-29T14:15:43","modified_gmt":"2021-06-29T14:15:43","slug":"accepted-papers","status":"publish","type":"page","link":"https:\/\/easyconferences.eu\/itp2021\/accepted-papers\/","title":{"rendered":"Accepted Papers"},"content":{"rendered":"

[et_pb_section fb_built=”1″ next_background_color=”#ffffff” _builder_version=”4.4.6″ background_color=”#8c8c8c” top_divider_color=”#b53319″ bottom_divider_style=”arrow3″][et_pb_row _builder_version=”4.4.6″ custom_margin=”-26px|auto||auto||”][et_pb_column type=”4_4″ _builder_version=”4.4.6″][et_pb_text _builder_version=”4.4.6″]<\/p>\n

ITP 2021 Accepted Papers<\/span><\/strong><\/h2>\n

[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section fb_built=”1″ _builder_version=”4.4.6″][et_pb_row _builder_version=”4.4.6″][et_pb_column type=”4_4″ _builder_version=”4.4.6″][et_pb_text _builder_version=”4.4.6″ hover_enabled=”0″]<\/p>\n

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks<\/a> –<\/strong>\u00a0<\/span>Andreas Lochbihler<\/a>.\u00a0<\/span><\/span><\/div>\n
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm<\/a> –<\/strong>\u00a0<\/span>Katherine Cordwell<\/a>,\u00a0Yong Kiam Tan<\/a>\u00a0and\u00a0Andr\u00e9 Platzer<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
Unsolvability of the Quintic Formalized in Dependent Type Theory<\/a> –\u00a0<\/span><\/strong>Sophie Bernard,\u00a0Cyril Cohen<\/a>,\u00a0Assia Mahboubi<\/a>\u00a0and\u00a0Pierre-Yves Strub<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
Verified Double Sided Auctions for Financial Markets<\/a> –<\/strong>\u00a0<\/span>Raja Natarajan<\/a>,\u00a0Suneel Sarswat<\/a>\u00a0and\u00a0Abhishek Kr Singh<\/a><\/span>.<\/span><\/div>\n
Complete Bidirectional Typing for the Calculus of Inductive Constructions<\/a> –<\/strong>\u00a0<\/span>Meven Lennon-Bertrand<\/a>.\u00a0<\/span><\/span><\/div>\n
Syntactic-semantic Form of Mizar Articles<\/a> –\u00a0<\/span><\/strong>Czes\u0142aw Byli\u0144ski,\u00a0Artur Korni\u0142owicz<\/a>\u00a0and\u00a0Adam Naumowicz<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
Proving Quantum Programs Correct<\/a> –<\/strong>\u00a0<\/span>Kesha Hietala<\/a>,\u00a0Robert Rand<\/a>, Shih-Han Hung, Liyi Li and\u00a0Michael Hicks<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
Proof Pearl : Playing with the Tower of Hanoi Formally<\/a> –<\/strong>\u00a0<\/span>Laurent Th\u00e9ry<\/a>.\u00a0<\/span><\/span><\/div>\n
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq<\/a> –<\/strong> Dominik Kirst<\/a>\u00a0and\u00a0Marc Hermes<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
A formal proof of modal completeness for provability logic<\/a> –\u00a0<\/span><\/strong>Marco Maggesi<\/a>\u00a0and\u00a0Cosimo Perini Brogi<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
Formalising a Turing-Complete Choreographic Language in Coq<\/a> –<\/strong>\u00a0<\/span>Lu\u00eds Cruz-Filipe<\/a>,\u00a0Fabrizio Montesi<\/a>\u00a0and\u00a0Marco Peressotti<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
A formalization of Dedekind domains and class groups of global fields<\/a> –<\/strong>\u00a0<\/span>Anne Baanen<\/a>,\u00a0Sander R. Dahmen<\/a>,\u00a0Filippo A. E. Nuccio Mortarino Majno di Capriglio<\/a>\u00a0and Ashvni Narayanan<\/span>.<\/span><\/div>\n
Formalization of Basic Combinatorics on Words<\/a> –<\/strong>\u00a0<\/span>Stepan Holub<\/a>\u00a0and Stepan Starosta<\/span>.\u00a0<\/span><\/span><\/div>\n
Reaching for the Star: Tale of a Monad in Coq<\/a> –\u00a0<\/span><\/strong>Pierre Nigron and Pierre-Evariste Dagand<\/span>.\u00a0<\/span><\/span><\/div>\n
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq<\/a> –<\/strong>\u00a0<\/span>Lennard G\u00e4her<\/a>\u00a0and\u00a0Fabian Kunze<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
Homotopy Type Theory in Isabelle (Short Paper)<\/a> –<\/strong>\u00a0<\/span>Joshua Chen<\/a>.<\/span><\/div>\n
Flexible coinduction in Agda<\/a> –<\/strong>\u00a0<\/span>Luca Ciccone,\u00a0Francesco Dagnino<\/a>\u00a0and\u00a0Elena Zucca<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
Verified Progress Tracking for Timely Dataflow<\/a> –<\/strong>\u00a0<\/span>Matthias Brun, S\u00e1ra Decova, Andrea Lattuada and\u00a0Dmitriy Traytel<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
A Variant of Wagner\u2019s Theorem Based on Combinatorial Hypermaps<\/a> –<\/strong>\u00a0<\/span>Christian Doczkal<\/a>.\u00a0<\/span><\/span><\/div>\n
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche<\/a> –<\/strong>\u00a0<\/span>Peter Koepke<\/a>, Adrian De Lon and\u00a0Anton Lorenzen<\/a><\/span>.\u00a0<\/span><\/span><\/div>\n
Itauto: an Extensible Intuitionistic SAT Solver<\/a> –<\/strong>\u00a0<\/span>Fr\u00e9d\u00e9ric Besson.\u00a0<\/span><\/span><\/div>\n
Verifying an HTTP Key-Value Server with Interaction Trees and VST<\/a> –<\/strong>\u00a0<\/span>Hengchu Zhang, Wolf Honor\u00e9, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce and Steve Zdancewic<\/span>.<\/span><\/div>\n
Value-oriented Legal Argumentation in Isabelle\/HOL<\/a> –<\/strong>\u00a0<\/span>Christoph Benzm\u00fcller<\/a>\u00a0and David Fuenmayor<\/span>.\u00a0<\/span><\/span><\/div>\n
Formalized Haar Measure<\/strong><\/a> –\u00a0<\/span>Floris van Doorn<\/a>.\u00a0<\/span><\/span><\/div>\n
A graphical user interface framework for formal verification<\/a> –<\/strong>\u00a0<\/span>Edward William Ayers,\u00a0Mateja Jamnik<\/a>\u00a0and William Gowers<\/span>.<\/span><\/div>\n
Formal Verification of Termination Criteria for First-Order Recursive Functions<\/a> –\u00a0<\/span><\/strong>Cesar Munoz<\/a>,\u00a0Mauricio Ayala-Rinc\u00f3n<\/a>, Mariano Moscato,\u00a0Aaron Dutle<\/a>, Anthony Narkawicz, Ariane Alves Almeida, Andreia B. Avelar da Silva and Thiago M. Ferreira Ramos<\/span>.<\/span><\/div>\n
Specifying Message Formats with Contiguity Types<\/a> –<\/strong>\u00a0<\/span>Konrad Slind.\u00a0<\/span><\/span><\/div>\n
A Formally Verified Checker for First-Order Proofs<\/strong><\/a>\u00a0<\/span>–<\/strong>\u00a0Seulkee Baek.\u00a0<\/div>\n
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value \u03bb-Calculus<\/a> –<\/strong>\u00a0<\/span>Yannick Forster<\/a>,\u00a0Fabian Kunze<\/a>,\u00a0Gert Smolka<\/a>\u00a0and Maximilian Wuttke<\/span>.\u00a0<\/span><\/span><\/div>\n

[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section fb_built=”1″ _builder_version=”4.4.6″][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"

ITP 2021 Accepted PapersA Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks –\u00a0Andreas Lochbihler.\u00a0 A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm –\u00a0Katherine Cordwell,\u00a0Yong Kiam Tan\u00a0and\u00a0Andr\u00e9 Platzer.\u00a0 Unsolvability of the Quintic Formalized in Dependent Type Theory –\u00a0Sophie Bernard,\u00a0Cyril Cohen,\u00a0Assia Mahboubi\u00a0and\u00a0Pierre-Yves Strub.\u00a0 Verified Double Sided Auctions for Financial Markets –\u00a0Raja […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"","_et_gb_content_width":""},"_links":{"self":[{"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/pages\/366"}],"collection":[{"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/comments?post=366"}],"version-history":[{"count":5,"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/pages\/366\/revisions"}],"predecessor-version":[{"id":523,"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/pages\/366\/revisions\/523"}],"wp:attachment":[{"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/media?parent=366"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}