Abstract is missing.
- Error Analysis of Digital Filters Using Theorem ProvingBehzad Akbarpour, Sofiène Tahar. 1-17 [doi]
- Verifying Uniqueness in a Logical FrameworkPenny Anderson, Frank Pfenning. 18-33 [doi]
- A Program Logic for Resource VerificationDavid Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano. 34-49 [doi]
- Proof Reuse with Extended Inductive TypesOlivier Boite. 50-65 [doi]
- Hierarchical ReflectionLuís Cruz-Filipe, Freek Wiedijk. 66-81 [doi]
- Correct Embedded Computing FuturesAl Davis. 82 [doi]
- Higher Order Rippling in IsaPlannerLucas Dixon, Jacques D. Fleuriot. 83-98 [doi]
- A Mechanical Proof of the Cook-Levin TheoremRuben Gamboa, John R. Cowles. 99-116 [doi]
- Formalizing the Proof of the Kepler ConjectureThomas C. Hales. 117 [doi]
- Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying CodeNadeem Abdul Hamid, Zhong Shao. 118-135 [doi]
- Extensible Hierarchical Tactic Construction in a Logical FrameworkJason Hickey, Aleksey Nogin. 136-151 [doi]
- Theorem Reuse by Proof Term TransformationEinar Broch Johnsen, Christoph Lüth. 152-167 [doi]
- Proving Compatibility Using RefinementMichael Jones, Aaron Benson, Dan Delorey. 168-183 [doi]
- Java Program Verification via a JVM Deep Embedding in ACL2Hanbing Liu, J. Strother Moore. 184-200 [doi]
- Reasoning About CBV Functional Programs in Isabelle/HOLJohn Longley, Randy Pollack. 201-216 [doi]
- Proof Pearl: From Concrete to Functional UnparsingJean-François Monin. 217-224 [doi]
- A Decision Procedure for Geometry in CoqJulien Narboux. 225-240 [doi]
- Recursive Function Definition for Types with BindersMichael Norrish. 241-256 [doi]
- Abstractions for Fault-Tolerant Distributed System VerificationLee Pike, Jeffrey Maddalon, Paul S. Miner, Alfons Geser. 257-270 [doi]
- Formalizing Integration Theory with an Application to Probabilistic AlgorithmsStefan Richter. 271-286 [doi]
- Formalizing Java Dynamic Loading in HOLTian-jun Zuo, Jun Gang Han, Ping Chen. 287-304 [doi]
- Certifying Machine Code Safety: Shallow Versus Deep EmbeddingMartin Wildmoser, Tobias Nipkow. 305-320 [doi]
- Term Algebras with Length Function and Bounded Quantifier AlternationTing Zhang, Henny B. Sipma, Zohar Manna. 321-336 [doi]