Abstract is missing.
- Erratum to: Interactive Theorem ProvingJeremy Avigad, Assia Mahboubi. [doi]
- Physical Addressing on Real Hardware in Isabelle/HOLReto Achermann, Lukas Humbel, David Cock, Timothy Roscoe. 1-19 [doi]
- Towards Certified Meta-Programming with Typed Template-CoqAbhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau. 20-39 [doi]
- Formalizing Ring Theory in PVSAndréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino. 40-47 [doi]
- Software Tool Support for Modular Reasoning in Modal Logics of ActionsSamuel Balco, Sabine Frittella, Giuseppe Greco 0001, Alexander Kurz 0001, Alessandra Palmigiano. 48-67 [doi]
- Backwards and Forwards with Separation LogicCallum Bannister, Peter Höfner, Gerwin Klein. 68-87 [doi]
- A Coq Formalisation of SQL's Execution EnginesVéronique Benzaken, Evelyne Contejean, Ch. Keller, E. Martins. 88-107 [doi]
- A Coq Tactic for Equality Learning in Linear ArithmeticSylvain Boulmé, Alexandre Maréchal. 108-125 [doi]
- The Coinductive Formulation of Common KnowledgeColm Baston, Venanzio Capretta. 126-141 [doi]
- Tactics and Certificates in Meta DeduktiRaphaël Cauderlier. 142-159 [doi]
- A Formalization of the LLL Basis Reduction AlgorithmJose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002. 160-177 [doi]
- A Formal Proof of the Minor-Exclusion Property for Treewidth-Two GraphsChristian Doczkal, Guillaume Combette, Damien Pous. 178-195 [doi]
- Verified Analysis of Random Binary Tree StructuresManuel Eberl, Max W. Haslbeck, Tobias Nipkow. 196-214 [doi]
- HOL Light QEJacques Carette, William M. Farmer, Patrick Laskowski. 215-234 [doi]
- Efficient Mendler-Style Lambda-Encodings in CedilleDenis Firsov, Richard Blair, Aaron Stump. 235-252 [doi]
- Verification of PCP-Related Computational Reductions in CoqYannick Forster 0002, Edith Heiter, Gert Smolka. 253-269 [doi]
- ProofWatch: Watchlist Guidance for Large Theories in EZarathustra Goertzel, Jan Jakubuv, Stephan Schulz 0001, Josef Urban. 270-288 [doi]
- Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of LtacJason Gross, Andres Erbsen, Adam Chlipala. 289-305 [doi]
- Verifying the LTL to Büchi Automata Translation via Very Weak Alternating AutomataSimon Jantsch, Michael Norrish. 306-323 [doi]
- CalcCheck: A Proof Checker for Teaching the "Logical Approach to Discrete Math"Wolfram Kahl. 324-341 [doi]
- Understanding Parameters of Deductive Verification: An Empirical Investigation of KeYAlexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer. 342-361 [doi]
- Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper)Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen. 362-369 [doi]
- Proof Pearl: Constructive Extraction of Cycle Finding AlgorithmsDominique Larchey-Wendling. 370-387 [doi]
- Fast Machine Words in Isabelle/HOLAndreas Lochbihler. 388-410 [doi]
- Relational Parametricity and Quotient Preservation for Modular (Co)datatypesAndreas Lochbihler, Joshua Schneider. 411-431 [doi]
- Towards Verified Handwritten Calculational Proofs - (Short Paper)Alexandra Mendes, João F. Ferreira. 432-440 [doi]
- A Formally Verified Solver for Homogeneous Linear Diophantine EquationsFlorian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel. 441-458 [doi]
- Formalizing Implicative Algebras in CoqÉtienne Miquey. 459-476 [doi]
- Boosting the Reuse of Formal SpecificationsMariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú. 477-494 [doi]
- Towards Formal Foundations for Game TheoryJulian Parsert, Cezary Kaliszyk. 495-503 [doi]
- Verified Timing Transformations in Synchronous Circuits with \lambda \pi -WareJoão Paulo Pizani Flor, Wouter Swierstra. 504-522 [doi]
- A Formal Equational Theory for Call-By-Push-ValueChristine Rizkallah, Dmitri Garbuzov, Steve Zdancewic. 523-541 [doi]
- Program Verification in the Presence of Cached Address TranslationHira Taqdees Syeda, Gerwin Klein. 542-559 [doi]
- Verified Tail Bounds for Randomized ProgramsJoseph Tassarotti, Robert Harper. 560-578 [doi]
- Verified Memoization and Dynamic ProgrammingSimon Wimmer, Shuwei Hu, Tobias Nipkow. 579-596 [doi]
- MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)Simon Wimmer, Johannes Hölzl. 597-603 [doi]
- Formalization of a Polymorphic Subtyping AlgorithmJinxu Zhao, Bruno C. D. S. Oliveira, Tom Schrijvers. 604-622 [doi]
- An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point TheoryRan Zmigrod, Matthew L. Daggitt, Timothy G. Griffin. 623-639 [doi]