More Web Proxy on the site http://driver.im/

default search action

combined dblp search
author search
venue search
publication search

ask others

16th TPHOLs 2003: Rom, Italy

> Home > Conferences and Workshops > TPHOLs

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/2003
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/2003
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

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/AbrialC03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/AbrialC03
Jean-Raymond Abrial, Dominique Cansell:
Click'n Prove: Interactive Proofs within Set Theory. 1-24

Hardware and Assembler Languages

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Fox03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Fox03
Anthony C. J. Fox:
Formal Specification and Verification of ARM6. 25-40
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Quigley03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Quigley03
Claire Louise Quigley:
A Programming Logic for Java Bytecode Programs. 41-54
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/KleinW03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/KleinW03
Gerwin Klein, Martin Wildmoser:
Verified Bytecode Subroutines. 55-70

Proof Automation I

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Norrish03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Norrish03
Michael Norrish:
Complete Integer Decision Procedures as Derived Rules in HOL. 71-86
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Magaud03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Magaud03
Nicolas Magaud:
Changing Data Representation within the Coq System. 87-102
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/SlindH03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/SlindH03
Konrad Slind, Joe Hurd:
Applications of Polytypism in Theorem Proving. 103-119

Proof Automation II

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/SchurmannP03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/SchurmannP03
Carsten Schürmann, Frank Pfenning:
A Coverage Checking Algorithm for LF. 120-135
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/KapurS03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/KapurS03
Deepak Kapur, Nikita A. Sakhanenko:
Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions. 136-154

Tool Combination

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/CacheraP03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/CacheraP03
David Cachera, David Pichardie:
Embedding of Systems of Affine Recurrence Equations in Coq. 155-170
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Amjad03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Amjad03
Hasan Amjad:
Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. 171-187
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/DybjerHT03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/DybjerHT03
Peter Dybjer, Qiao Haiyan, Makoto Takeyama:
Combining Testing and Proving in Dependent Type Theory. 188-203

Invited Talk II

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Miller03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Miller03
Dale Miller:
Reasoning about Proof Search Specifications: An Abstract. 204

Logic Extensions

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Cruz-FilipeS03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Cruz-FilipeS03
Luís Cruz-Filipe, Bas Spitters:
Program Extraction from Large Proof Developments. 205-220
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/WiedijkZ03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/WiedijkZ03
Freek Wiedijk, Jan Zwanenburg:
First Order Logic with Domain Conditions. 221-237
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Reed03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Reed03
Jason Reed:
Extending Higher-Order Unification to Support Proof Irrelevance. 238-252

Advances in Theorem Prover Technology

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/KrsticM03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/KrsticM03
Sava Krstic, John Matthews:
Inductive Invariants for Nested Recursion. 253-269
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Chrzaszcz03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Chrzaszcz03
Jacek Chrzaszcz:
Implementing Modules in the Coq System. 270-286
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/HickeyNCABBEGKKKLSWY03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/HickeyNCABBEGKKKLSWY03
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

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Thery03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Thery03
Laurent Théry:
Proving Pearl: Knuth's Algorithm for Prime Numbers. 304-318
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/MeikleF03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/MeikleF03
Laura I. Meikle, Jacques D. Fleuriot:
Formalizing Hilbert's Grundlagen in Isabelle/Isar. 319-334

Security

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/AndronickCL03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/AndronickCL03
June Andronick, Boutheina Chetali, Olivier Ly:
Using Coq to Verify Java Card Applet Isolation Properties. 335-351
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/BellaLP03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/BellaLP03
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.