Abstract is missing.
- Engineering Theories with Z3Nikolaj Bjørner. 1-2 [doi]
- Algebra, Logic, Locality, ConcurrencyPeter W. O'Hearn. 3-4 [doi]
- Constructive Formalization of Hybrid Logic with EventualitiesChristian Doczkal, Gert Smolka. 5-20 [doi]
- Proof-Carrying Code in a Session-Typed Process CalculusFrank Pfenning, Luís Caires, Bernardo Toninho. 21-36 [doi]
- Automated Certification of Implicit Induction ProofsSorin Stratulat, Vincent Demange. 37-53 [doi]
- A Proposal for Broad Spectrum Proof CertificatesDale Miller. 54-69 [doi]
- Univalent Semantics of Constructive Type TheoriesVladimir Voevodsky. 70 [doi]
- Formalization of Wu's Simple Method in CoqJean-David Génevaux, Julien Narboux, Pascal Schreck. 71-86 [doi]
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point TheoremCezary Kaliszyk, Henk Barendregt. 87-102 [doi]
- Simple, Functional, Sound and Complete Parsing for All Context-Free GrammarsTom Ridge. 103-118 [doi]
- A Decision Procedure for Regular Expression Equivalence in Type TheoryThierry Coquand, Vincent Siles. 119-134 [doi]
- A Modular Integration of SAT/SMT Solvers to Coq through Proof WitnessesMichaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner. 135-150 [doi]
- Modular SMT Proofs for Fast Reflexive Checking Inside CoqFrédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. 151-166 [doi]
- Tactics for Reasoning Modulo AC in CoqThomas Braibant, Damien Pous. 167-182 [doi]
- Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOLSascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber. 183-198 [doi]
- Teaching Experience: Logic and Formal Methods with CoqMartin Henz, Aquinas Hobor. 199-215 [doi]
- The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math"Wolfram Kahl. 216-230 [doi]
- VeriSmall: Verified Smallfoot Shape AnalysisAndrew W. Appel. 231-246 [doi]
- Verification of Scalable Synchronous QueueJinjiang Lei, Zongyan Qiu. 247-263 [doi]
- Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple InheritanceJieung Kim, Sukyoung Ryu. 264-279 [doi]
- Mechanizing the Metatheory of mini-XQueryJames Cheney, Christian Urban. 280-295 [doi]
- Automatically Verifying Typing Constraints for a Data Processing LanguageMichael Backes, Catalin Hritcu, Thorsten Tarrach. 296-313 [doi]
- Hardware-Dependent Proofs of Numerical ProgramsThi Minh Tuyen Nguyen, Claude Marché. 314-329 [doi]
- Coquet: A Coq Library for Verifying HardwareThomas Braibant. 330-345 [doi]
- First Steps towards the Certification of an ARM Simulator Using CompcertXiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui. 346-361 [doi]
- Full Reduction at Full ThrottleMathieu Boespflug, Maxime Dénès, Benjamin Grégoire. 362-377 [doi]
- Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion ResiliencePierre Corbineau, Mathilde Duclos, Yassine Lakhnech. 378-393 [doi]
- Proof Pearl: The Marriage TheoremDongchen Jiang, Tobias Nipkow. 394-399 [doi]