Abstract is missing.
- On the Correctness of Operating System KernelsMauro Gargano, Mark A. Hillebrand, Dirk Leinenbach, Wolfgang J. Paul. 1-16 [doi]
- Alpha-Structural Recursion and InductionAndrew M. Pitts. 17-34 [doi]
- Shallow Lazy ProofsHasan Amjad. 35-49 [doi]
- Mechanized Metatheory for the Masses: The PoplMark ChallengeBrian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic. 50-65 [doi]
- A Structured Set of Higher-Order ProblemsChristoph Benzmüller, Chad E. Brown. 66-81 [doi]
- Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVSNéstor Cataño. 82-97 [doi]
- Proving Equalities in a Commutative Ring Done Right in CoqBenjamin Grégoire, Assia Mahboubi. 98-113 [doi]
- A HOL Theory of Euclidean SpaceJohn Harrison. 114-129 [doi]
- A Design Structure for Higher Order QuotientsPeter V. Homeier. 130-146 [doi]
- Axiomatic Constructor Classes in Isabelle/HOLCFBrian Huffman, John Matthews, Peter White. 147-162 [doi]
- Meta Reasoning in ACL2Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith. 163-178 [doi]
- Reasoning About Java Programs with Aliasing and Frame ConditionsClaude Marché, Christine Paulin-Mohring. 179-194 [doi]
- Real Number Calculations and Theorem ProvingCésar Muñoz, David Lester. 195-210 [doi]
- Verifying a Secure Information Flow AnalyzerDavid A. Naumann. 211-226 [doi]
- Proving Bounds for Real Linear Programs in Isabelle/HOLSteven Obua. 227-244 [doi]
- Essential Incompleteness of Arithmetic Verified by CoqRussell O Connor. 245-260 [doi]
- Verification of BDD NormalizationVeronika Ortner, Norbert Schirmer. 261-277 [doi]
- Extensionality in the Calculus of ConstructionsNicolas Oury. 278-293 [doi]
- A Mechanically Verified, Sound and Complete Theorem Prover for First Order LogicTom Ridge, James Margetson. 294-309 [doi]
- A Generic Network on Chip ModelJulien Schmaltz, Dominique Borrione. 310-325 [doi]
- Formal Verification of a SHA-1 Circuit Core Using ACL2Diana Toma, Dominique Borrione. 326-341 [doi]
- From PSL to LTL: A Formal Validation in HOLThomas Tuerk, Klaus Schneider. 342-357 [doi]
- Proof Pearl: A Formal Proof of Higman s Lemma in ACL2Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo. 358-372 [doi]
- Proof Pearl: Dijkstra s Shortest Path Algorithm Verified with ACL2J. Strother Moore, Qiang Zhang. 373-384 [doi]
- Proof Pearl: Defining Functions over Finite SetsTobias Nipkow, Lawrence C. Paulson. 385-396 [doi]
- Proof Pearl: Using Combinators to Manipulate let-Expressions in ProofMichael Norrish, Konrad Slind. 397-408 [doi]