16. TPHOLs 2003: Rom, Italy

Invited Talk I

• Jean-Raymond Abrial, Dominique Cansell:
  Click'n Prove: Interactive Proofs within Set Theory. 1-24
  

Hardware and Assembler Languages

• Anthony C. J. Fox:
  Formal Specification and Verification of ARM6. 25-40
  
• Claire L. Quigley:
  A Programming Logic for Java Bytecode Programs. 41-54
  
• Gerwin Klein, Martin Wildmoser:
  Verified Bytecode Subroutines. 55-70
  

Proof Automation I

• Michael Norrish:
  Complete Integer Decision Procedures as Derived Rules in HOL. 71-86
  
• Nicolas Magaud:
  Changing Data Representation within the Coq System. 87-102
  
• Konrad Slind, Joe Hurd:
  Applications of Polytypism in Theorem Proving. 103-119
  

Proof Automation II

• Carsten Schürmann, Frank Pfenning:
  A Coverage Checking Algorithm for LF. 120-135
  
• Deepak Kapur, Nikita A. Sakhanenko:
  Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions. 136-154
  

Tool Combination

• David Cachera, David Pichardie:
  Embedding of Systems of Affine Recurrence Equations in Coq. 155-170
  
• Hasan Amjad:
  Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. 171-187
  
• Peter Dybjer, Qiao Haiyan, Makoto Takeyama:
  Combining Testing and Proving in Dependent Type Theory. 188-203
  

Invited Talk II

• Dale Miller:
  Reasoning about Proof Search Specifications: An Abstract. 204
  

Logic Extensions

• Luís Cruz-Filipe, Bas Spitters:
  Program Extraction from Large Proof Developments. 205-220
  
• Freek Wiedijk, Jan Zwanenburg:
  First Order Logic with Domain Conditions. 221-237
  
• Jason Reed:
  Extending Higher-Order Unification to Support Proof Irrelevance. 238-252
  

Advances in Theorem Prover Technology

• Sava Krstic, John Matthews:
  Inductive Invariants for Nested Recursion. 253-269
  
• Jacek Chrzaszcz:
  Implementing Modules in the Coq System. 270-286
  
• Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, Xin Yu:
  MetaPRL - A Modular Logical Environment. 287-303
  

Mathematical Theories

• Laurent Théry:
  Proving Pearl: Knuth's Algorithm for Prime Numbers. 304-318
  
• Laura I. Meikle, Jacques D. Fleuriot:
  Formalizing Hilbert's Grundlagen in Isabelle/Isar. 319-334
  

Security

• June Andronick, Boutheina Chetali, Olivier Ly:
  Using Coq to Verify Java Card Applet Isolation Properties. 335-351
  
• Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson:
  Verifying Second-Level Security Protocols. 352-366