Abstract is missing.
- MetiTarski: Past and FutureLawrence C. Paulson. 1-10 [doi]
- Computer-Aided Cryptographic ProofsGilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin. 11-27 [doi]
- A Differential Operator Approach to Equational Differential Invariants - (Invited Paper)André Platzer. 28-48 [doi]
- Abella: A TutorialAndrew Gacek. 49-50 [doi]
- A Cantor Trio: Denumerability, the Reals, and the Real Algebraic NumbersRuben Gamboa, John R. Cowles. 51-66 [doi]
- Construction of Real Algebraic Numbers in CoqCyril Cohen. 67-82 [doi]
- A Refinement-Based Approach to Computational Algebra in CoqMaxime Dénès, Anders Mörtberg, Vincent Siles. 83-98 [doi]
- Bridging the Gap: Automatic Verified Abstraction of CDavid Greenaway, June Andronick, Gerwin Klein. 99-115 [doi]
- Abstract Interpretation of Annotated CommandsTobias Nipkow. 116-132 [doi]
- Verifying and Generating WP Transformers for Procedures on Complex DataPatrick Michel, Arnd Poetzsch-Heffter. 133-148 [doi]
- Bag Equivalence via a Proof-Relevant Membership RelationNils Anders Danielsson. 149-165 [doi]
- Applying Data Refinement for Monadic Programs to Hopcroft's AlgorithmPeter Lammich, Thomas Tuerk. 166-182 [doi]
- Synthesis of Distributed Mobile Programs Using Monadic Types in CoqMarino Miculan, Marco Paviotti. 183-200 [doi]
- Towards Provably Robust WatermarkingDavid Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring. 201-216 [doi]
- Priority Inheritance Protocol Proved CorrectXingyuan Zhang, Christian Urban, Chunhan Wu. 217-232 [doi]
- Formalization of Shannon's Theorems in SSReflect-CoqReynald Affeldt, Manabu Hagiwara. 233-249 [doi]
- Stop When You Are Almost-Full - Adventures in Constructive TerminationDimitrios Vytiniotis, Thierry Coquand, David Wahlstedt. 250-265 [doi]
- Certification of Nontermination ProofsChristian Sternagel, René Thiemann. 266-282 [doi]
- A Compact Proof of Decidability for Regular Expression EquivalenceAndrea Asperti. 283-298 [doi]
- Using Locales to Define a Rely-Guarantee Temporal LogicWilliam Mansky, Elsa L. Gunter. 299-314 [doi]
- Charge! - A Framework for Higher-Order Separation Logic in CoqJesper Bengtson, Jonas Braband Jensen, Lars Birkedal. 315-331 [doi]
- Mechanised Separation AlgebraGerwin Klein, Rafal Kolanski, Andrew Boyton. 332-337 [doi]
- Directions in ISA SpecificationAnthony C. J. Fox. 338-344 [doi]
- More SPASS with Isabelle - Superposition with Hard Sorts and Configurable SimplificationJasmin Christian Blanchette, Andrei Popescu 0001, Daniel Wand, Christoph Weidenbach. 345-360 [doi]
- A Language of Patterns for Subterm SelectionGeorges Gonthier, Enrico Tassi. 361-376 [doi]
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOLFabian Immler, Johannes Hölzl. 377-392 [doi]
- Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number TheoremLars Noschinski. 393-404 [doi]
- Standalone Tactics Using OpenTheoryRamana Kumar, Joe Hurd. 405-411 [doi]
- Functional Programs: Conversions between Deep and Shallow EmbeddingsMagnus O. Myreen. 412-417 [doi]