16. TPHOLs 2003: Rom, Italy

David A. Basin, Burkhart Wolff (Eds.): Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings. Lecture Notes in Computer Science 2758 Springer 2003, ISBN 3-540-40664-6

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

Last update Fri May 24 19:52:39 2013 CET by the DBLP Team —

This material is Open Data

Data released under the ODC-BY 1.0 license — See also our legal information page