Abstract is missing.
- Applying Formal Methods in the LargeDominique Bolignano. 1 [doi]
- Automating Theorem Proving with SMTK. Rustan M. Leino. 2-16 [doi]
- Certifying Voting ProtocolsCarsten Schürmann. 17 [doi]
- Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future OpportunitiesPanagiotis Manolios. 18 [doi]
- Canonical Structures for the Working Coq UserAssia Mahboubi, Enrico Tassi. 19-34 [doi]
- MaSh: Machine Learning for SledgehammerDaniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban. 35-50 [doi]
- Scalable LCF-Style Proof TranslationCezary Kaliszyk, Alexander Krauss. 51-66 [doi]
- Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful ComputationGuillaume Claret, Lourdes Del Carmen González-Huesca, Yann Régis-Gianas, Beta Ziliani. 67-83 [doi]
- Automatic Data RefinementPeter Lammich. 84-99 [doi]
- Data Refinement in Isabelle/HOLFlorian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow. 100-115 [doi]
- Light-Weight Containers for Isabelle: Efficient, Extensible, NestableAndreas Lochbihler. 116-132 [doi]
- Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1Michael Norrish, Brian Huffman. 133-146 [doi]
- Mechanising Turing Machines and Computability Theory in Isabelle/HOLJian Xu, Xingyuan Zhang, Christian Urban. 147-162 [doi]
- A Machine-Checked Proof of the Odd Order TheoremGeorges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry. 163-179 [doi]
- Kleene Algebra with Tests and Coq Tools for while ProgramsDamien Pous. 180-196 [doi]
- Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOLAlasdair Armstrong, Georg Struth, Tjark Weber. 197-212 [doi]
- Pragmatic Quotient Types in CoqCyril Cohen. 213-228 [doi]
- Mechanical Verification of SAT Refutations with Extended ResolutionNathan Wetzler, Marijn Heule, Warren A. Hunt Jr.. 229-244 [doi]
- Formalizing Bounded IncreaseRené Thiemann. 245-260 [doi]
- Formal Program Optimization in Nuprl Using Computational Equivalence and Partial TypesVincent Rahli, Mark Bickford, Abhishek Anand. 261-278 [doi]
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOLJohannes Hölzl, Fabian Immler, Brian Huffman. 279-294 [doi]
- Formal Reasoning about Classified Markov Chains in HOLLiya Liu, Osman Hasan, Vincent Aravantinos, Sofiène Tahar. 295-310 [doi]
- Practical Probability: Applying pGCL to Lattice SchedulingDavid Cock. 311-327 [doi]
- Adjustable ReferencesViktor Vafeiadis. 328-337 [doi]
- Handcrafted Inversions Made Operational on Operational SemanticsJean-François Monin, Xiaomu Shi. 338-353 [doi]
- Circular Coinduction in Coq Using Bisimulation-Up-To TechniquesJörg Endrullis, Dimitri Hendriks, Martin Bodin. 354-369 [doi]
- Program Extraction from Nested DefinitionsKenji Miyamoto, Fredrik Nordvall Forsberg, Helmut Schwichtenberg. 370-385 [doi]
- Subformula Linking as an Interaction MethodKaustuv Chaudhuri. 386-401 [doi]
- Automatically Generated Infrastructure for De Bruijn SyntaxesEmmanuel Polonowski. 402-417 [doi]
- Shared-Memory Multiprocessing for Interactive Theorem ProvingMakarius Wenzel. 418-434 [doi]
- A Parallelized Theorem Prover for a Logic with Parallel ExecutionDavid L. Rager, Warren A. Hunt Jr., Matt Kaufmann. 435-450 [doi]
- Communicating Formal Proofs: The Case of FlyspeckCarst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers. 451-456 [doi]
- Square Root and Division Elimination in PVSPierre Néron. 457-462 [doi]
- The Picard Algorithm for Ordinary Differential Equations in CoqEvgeny Makarov, Bas Spitters. 463-468 [doi]
- Stateless Higher-Order Logic with Quantified TypesEvan Austin, Perry Alexander. 469-476 [doi]
- Implementing Hash-Consed Structures in CoqThomas Braibant, Jacques-Henri Jourdan, David Monniaux. 477-483 [doi]
- Towards Certifying Network CalculusEtienne Mabille, Marc Boyer, Loïc Fejoz, Stephan Merz. 484-489 [doi]
- Steps towards Verified Implementations of HOL LightMagnus O. Myreen, Scott Owens, Ramana Kumar. 490-495 [doi]