Abstract is missing.
- Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial UsageThomas Kropf. 1-4 [doi]
- Disjoint Sums over Type Classes in HOLNorbert Völker. 5-18 [doi]
- Inductive Datatypes in HOL - Lessons Learned in Formal-Logic EngineeringStefan Berghofer, Markus Wenzel. 19-36 [doi]
- Isomorphisms - A Link Between the Shallow and the DeepThomas Santen. 37-54 [doi]
- Polytypic Proof ConstructionHolger Pfeifer, Harald Rueß. 55-72 [doi]
- Recursive Function Definition over Coinductive TypesJohn Matthews. 73-90 [doi]
- Hardware Verification Using Co-induction in COQSolange Coupet-Grimal, Line Jakubiec. 91-108 [doi]
- Connecting Proof Checkers and Computer Algebra Using OpenMathOlga Caprotti, Arjeh M. Cohen. 109-112 [doi]
- A Machine-Checked Theory of Floating Point ArithmeticJohn Harrison. 113-130 [doi]
- Universal Algebra in Type TheoryVenanzio Capretta. 131-148 [doi]
- Locales - A Sectioning Concept for IsabelleFlorian Kammüller, Markus Wenzel, Lawrence C. Paulson. 149-166 [doi]
- Isar - A Generic Interpretative Approach to Readable Formal Proof DocumentsMarkus Wenzel. 167-184 [doi]
- On the Implementation of an Extensible Declarative Proof LanguageVincent Zammit. 185-202 [doi]
- Three Tactic Theorem ProvingDon Syme. 203-220 [doi]
- Mechanized Operational Semantics via (Co)InductionSimon Ambler, Roy L. Crole. 221-238 [doi]
- Representing WP Semantics in Isabelle/ZFMark Staples. 239-254 [doi]
- A HOL Conversion for Translating Linear Time Temporal Logic to omega-AutomataKlaus Schneider, Dirk W. Hoffmann. 255-272 [doi]
- From I/O Automata to Timed I/O AutomataBernd Grobauer, Olaf Müller. 273-290 [doi]
- Formal Methods and Security Evaluation (Invited Talk)Dominique Bolignano. 291-292 [doi]
- Importing MDG Verification Results into HOLHaiyan Xiong, Paul Curzon, Sofiène Tahar. 293-310 [doi]
- Integrating Gandalf and HOLJoe Hurd. 311-322 [doi]
- Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem ProvingMark Aagaard, Robert B. Jones, Carl-Johan H. Seger. 323-340 [doi]
- Symbolic Functional EvaluationNancy A. Day, Jeffrey J. Joyce. 341-358 [doi]