default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID16th TPHOLs 2003: Rom, Italy
- David A. Basin, Burkhart Wolff:
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 Louise 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-03-28 23:33 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
