Abstract is missing.
- Let s Get Physical: Models and Methods for Real-World Security ProtocolsDavid A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt. 1-22 [doi]
- VCC: A Practical System for Verifying Concurrent CErnie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies. 23-42 [doi]
- Without Loss of GeneralityJohn Harrison. 43-59 [doi]
- HOL Light: An OverviewJohn Harrison. 60-66 [doi]
- A Brief Overview of MizarAdam Naumowicz, Artur Kornilowicz. 67-72 [doi]
- A Brief Overview of Agda - A Functional Language with Dependent TypesAna Bove, Peter Dybjer, Ulf Norell. 73-78 [doi]
- The Twelf Proof AssistantCarsten Schürmann. 79-83 [doi]
- Hints in UnificationAndrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi. 84-98 [doi]
- Psi-calculi in IsabelleJesper Bengtson, Joachim Parrow. 99-114 [doi]
- Some Domain Theory and Denotational Semantics in CoqNick Benton, Andrew Kennedy, Carsten Varming. 115-130 [doi]
- Turning Inductive into Equational SpecificationsStefan Berghofer, Lukas Bulwahn, Florian Haftmann. 131-146 [doi]
- Formalizing the Logic-Automaton ConnectionStefan Berghofer, Markus Reiter. 147-163 [doi]
- Extended First-Order LogicChad E. Brown, Gert Smolka. 164-179 [doi]
- Formalising Observer Theory for Environment-Sensitive BisimulationJeremy E. Dawson, Alwen Tiu. 180-195 [doi]
- Formal Certification of a Resource-Aware Language ImplementationJavier de Dios, Ricardo Peña-MarÃ. 196-211 [doi]
- A Certified Data Race Analysis for a Java-like LanguageFrédéric Dabrowski, David Pichardie. 212-227 [doi]
- Formal Analysis of Optical Waveguides in HOLOsman Hasan, Sanaz Khan Afshar, Sofiène Tahar. 228-243 [doi]
- The HOL-Omega LogicPeter V. Homeier. 244-259 [doi]
- A Purely Definitional Universal DomainBrian Huffman. 260-275 [doi]
- Types, Maps and Separation LogicRafal Kolanski, Gerwin Klein. 276-292 [doi]
- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive EquivalenceStéphane Le Roux. 293-309 [doi]
- Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOLAndreas Lochbihler. 310-326 [doi]
- Packaging Mathematical StructuresFrançois Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. 327-342 [doi]
- Practical Tactics for Separation LogicAndrew McCreight. 343-358 [doi]
- Verified LISP Implementations on ARM, x86 and PowerPCMagnus O. Myreen, Michael J. C. Gordon. 359-374 [doi]
- Trace-Based Coinductive Operational Semantics for WhileKeiko Nakata, Tarmo Uustalu. 375-390 [doi]
- A Better x86 Memory Model: x86-TSOScott Owens, Susmit Sarkar, Peter Sewell. 391-407 [doi]
- Formal Verification of Exact Computations Using Newton s MethodNicolas Julien, Ioana Pasca. 408-423 [doi]
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOLAlexander Schimpf, Stephan Merz, Jan-Georg Smaus. 424-439 [doi]
- A Hoare Logic for the State MonadWouter Swierstra. 440-451 [doi]
- Certification of Termination Proofs Using CeTARené Thiemann, Christian Sternagel. 452-468 [doi]
- A Formalisation of Smallfoot in HOLThomas Tuerk. 469-484 [doi]
- Liveness Reasoning with Isabelle/HOLJinshuang Wang, Huabing Yang, Xingyuan Zhang. 485-499 [doi]
- Mind the GapSimon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish. 500-515 [doi]