18. TPHOLs 2005: Oxford, UK

Invited Papers

• Mauro Gargano, Mark A. Hillebrand, Dirk Leinenbach, Wolfgang J. Paul:
  On the Correctness of Operating System Kernels. 1-16
  
• Andrew M. Pitts:
  Alpha-Structural Recursion and Induction. 17-34
  

Regular Papers

• Hasan Amjad:
  Shallow Lazy Proofs. 35-49
  
• Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic:
  Mechanized Metatheory for the Masses: The PoplMark Challenge. 50-65
  
• Christoph Benzmüller, Chad E. Brown:
  A Structured Set of Higher-Order Problems. 66-81
  
• Néstor Cataño:
  Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS. 82-97
  
• Benjamin Grégoire, Assia Mahboubi:
  Proving Equalities in a Commutative Ring Done Right in Coq. 98-113
  
• John Harrison:
  A HOL Theory of Euclidean Space. 114-129
  
• Peter V. Homeier:
  A Design Structure for Higher Order Quotients. 130-146
  
• Brian Huffman, John Matthews, Peter White:
  Axiomatic Constructor Classes in Isabelle/HOLCF. 147-162
  
• Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith:
  Meta Reasoning in ACL2. 163-178
  
• Claude Marché, Christine Paulin-Mohring:
  Reasoning About Java Programs with Aliasing and Frame Conditions. 179-194
  
• César Muñoz, David R. Lester:
  Real Number Calculations and Theorem Proving. 195-210
  
• David A. Naumann:
  Verifying a Secure Information Flow Analyzer. 211-226
  
• Steven Obua:
  Proving Bounds for Real Linear Programs in Isabelle/HOL. 227-244
  
• Russell O'Connor:
  Essential Incompleteness of Arithmetic Verified by Coq. 245-260
  
• Veronika Ortner, Norbert Schirmer:
  Verification of BDD Normalization. 261-277
  
• Nicolas Oury:
  Extensionality in the Calculus of Constructions. 278-293
  
• Tom Ridge, James Margetson:
  A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. 294-309
  
• Julien Schmaltz, Dominique Borrione:
  A Generic Network on Chip Model. 310-325
  
• Diana Toma, Dominique Borrione:
  Formal Verification of a SHA-1 Circuit Core Using ACL2. 326-341
  
• Thomas Tuerk, Klaus Schneider:
  From PSL to LTL: A Formal Validation in HOL. 342-357
  

Proof Pearls

• Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo:
  Proof Pearl: A Formal Proof of Higman's Lemma in ACL2. 358-372
  
• J. Strother Moore, Qiang Zhang:
  Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. 373-384
  
• Tobias Nipkow, Lawrence C. Paulson:
  Proof Pearl: Defining Functions over Finite Sets. 385-396
  
• Michael Norrish, Konrad Slind:
  Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. 397-408
  

Last update Fri May 25 08:43:22 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page