Abstract is missing.
- A Formally Verified OS Kernel. Now What?Gerwin Klein. 1-7 [doi]
- Proof Assistants as Teaching Assistants: A View from the TrenchesBenjamin C. Pierce. 8 [doi]
- A Certified Denotational Abstract InterpreterDavid Cachera, David Pichardie. 9-24 [doi]
- Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue MeasureJohn R. Cowles, Ruben Gamboa. 25-34 [doi]
- A New Foundation for Nominal IsabelleBrian Huffman, Christian Urban. 35-50 [doi]
- (Nominal) Unification by Recursive Descent with Triangular SubstitutionsRamana Kumar, Michael Norrish. 51-66 [doi]
- A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive NetworksFreek Verbeek, Julien Schmaltz. 67-82 [doi]
- Extending Coq with Imperative Features and Its Application to SAT VerificationMichaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry. 83-98 [doi]
- A Tactic Language for Declarative ProofsSerge Autexier, Dominik Dietrich. 99-114 [doi]
- Programming Language Techniques for Cryptographic ProofsGilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin. 115-130 [doi]
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model FinderJasmin Christian Blanchette, Tobias Nipkow. 131-146 [doi]
- Formal Proof of a Wave Equation Resolution Scheme: The Method ErrorSylvie Boldo, François Clément, Jean-Christophe Filliåtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis. 147-162 [doi]
- An Efficient Coq Tactic for Deciding Kleene AlgebrasThomas Braibant, Damien Pous. 163-178 [doi]
- Fast LCF-Style Proof Reconstruction for Z3Sascha Böhme, Tjark Weber. 179-194 [doi]
- The Optimal Fixed Point CombinatorArthur Charguéraud. 195-210 [doi]
- Formal Study of Plane Delaunay TriangulationJean-François Dufourd, Yves Bertot. 211-226 [doi]
- Reasoning with Higher-Order Abstract Syntax and Contexts: A ComparisonAmy P. Felty, Brigitte Pientka. 227-242 [doi]
- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set ArchitectureAnthony C. J. Fox, Magnus O. Myreen. 243-258 [doi]
- Automated Machine-Checked Hybrid System Safety ProofsHerman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen. 259-274 [doi]
- Coverset Induction with Partiality and Subsorts: A Powerlist Case StudyJoe Hendrix, Deepak Kapur, José Meseguer. 275-290 [doi]
- Case-Analysis for Rippling and Inductive ProofMoa Johansson, Lucas Dixon, Alan Bundy. 291-306 [doi]
- Importing HOL Light into CoqChantal Keller, Benjamin Werner. 307-322 [doi]
- A Mechanized Translation from Higher-Order Logic to Set TheoryAlexander Krauss, Andreas Schropp. 323-338 [doi]
- The Isabelle Collections FrameworkPeter Lammich, Andreas Lochbihler. 339-354 [doi]
- Interactive Termination Proofs Using Termination CoresPanagiotis Manolios, Daron Vroon. 355-370 [doi]
- A Framework for Formal Verification of Compiler OptimizationsWilliam Mansky, Elsa L. Gunter. 371-386 [doi]
- On the Formalization of the Lebesgue Integration Theory in HOLTarek Mhamdi, Osman Hasan, Sofiène Tahar. 387-402 [doi]
- From Total Store Order to Sequential Consistency: A Practical Reduction TheoremErnie Cohen, Bert Schirmer. 403-418 [doi]
- Equations: A Dependent Pattern-Matching CompilerMatthieu Sozeau. 419-434 [doi]
- A Mechanically Verified AIG-to-BDD Conversion AlgorithmSol Swords, Warren A. Hunt Jr.. 435-449 [doi]
- Inductive Consequences in the Calculus of ConstructionsDaria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz. 450-465 [doi]
- Validating QBF Invalidity in HOL4Tjark Weber. 466-480 [doi]
- Higher-Order Abstract Syntax in Isabelle/HOLDouglas J. Howe. 481-484 [doi]
- Separation Logic Adapted for Proofs by RewritingMagnus O. Myreen. 485-489 [doi]
- Developing the Algebraic Hierarchy with Type Classes in CoqBas Spitters, Eelis van der Weegen. 490-493 [doi]