ask others

22. TPHOLs 2009: Munich, Germany

> Home > Conferences and Workshops > TPHOLs

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/2009
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/2009
Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel:
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science 5674, Springer 2009, ISBN 978-3-642-03358-2

Invited Papers

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BasinCSS09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BasinCSS09
David A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt:
Let's Get Physical: Models and Methods for Real-World Security Protocols. 1-22
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/CohenDHLMSST09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/CohenDHLMSST09
Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies:
VCC: A Practical System for Verifying Concurrent C. 23-42
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Harrison09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Harrison09
John Harrison:
Without Loss of Generality. 43-59

Invited Tutorials

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Harrison09a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Harrison09a
John Harrison:
HOL Light: An Overview. 60-66
- view
  - electronic edition via DOI
  - electronic edition @ wikidata.org
- export record
  dblp key:
  - conf/tphol/NaumowiczK09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/NaumowiczK09
Adam Naumowicz, Artur Kornilowicz:
A Brief Overview of Mizar. 67-72
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BoveDN09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BoveDN09
Ana Bove, Peter Dybjer, Ulf Norell:
A Brief Overview of Agda - A Functional Language with Dependent Types. 73-78
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Schurmann09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Schurmann09
Carsten Schürmann:
The Twelf Proof Assistant. 79-83

Regular Papers

- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/AspertiRCT09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/AspertiRCT09
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi:
Hints in Unification. 84-98
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BengtsonP09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BengtsonP09
Jesper Bengtson, Joachim Parrow:
Psi-calculi in Isabelle. 99-114
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BentonKV09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BentonKV09
Nick Benton, Andrew Kennedy, Carsten Varming:
Some Domain Theory and Denotational Semantics in Coq. 115-130
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BerghoferBH09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BerghoferBH09
Stefan Berghofer, Lukas Bulwahn, Florian Haftmann:
Turning Inductive into Equational Specifications. 131-146
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BerghoferR09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BerghoferR09
Stefan Berghofer, Markus Reiter:
Formalizing the Logic-Automaton Connection. 147-163
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/BrownS09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/BrownS09
Chad E. Brown, Gert Smolka:
Extended First-Order Logic. 164-179
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/DawsonT09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/DawsonT09
Jeremy E. Dawson, Alwen Tiu:
Formalising Observer Theory for Environment-Sensitive Bisimulation. 180-195
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/DiosP09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/DiosP09
Javier de Dios, Ricardo Peña-Marí:
Formal Certification of a Resource-Aware Language Implementation. 196-211
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/DabrowskiP09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/DabrowskiP09
Frédéric Dabrowski, David Pichardie:
A Certified Data Race Analysis for a Java-like Language. 212-227
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/HasanAT09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/HasanAT09
Osman Hasan, Sanaz Khan Afshar, Sofiène Tahar:
Formal Analysis of Optical Waveguides in HOL. 228-243
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Homeier09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Homeier09
Peter V. Homeier:
The HOL-Omega Logic. 244-259
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Huffman09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Huffman09
Brian Huffman:
A Purely Definitional Universal Domain. 260-275
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/KolanskiK09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/KolanskiK09
Rafal Kolanski, Gerwin Klein:
Types, Maps and Separation Logic. 276-292
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Roux09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Roux09
Stéphane Le Roux:
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence. 293-309
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Lochbihler09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Lochbihler09
Andreas Lochbihler:
Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. 310-326
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/GarillotGMR09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/GarillotGMR09
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau:
Packaging Mathematical Structures. 327-342
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/McCreight09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/McCreight09
Andrew McCreight:
Practical Tactics for Separation Logic. 343-358
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/MyreenG09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/MyreenG09
Magnus O. Myreen, Michael J. C. Gordon:
Verified LISP Implementations on ARM, x86 and PowerPC. 359-374
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/NakataU09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/NakataU09
Keiko Nakata, Tarmo Uustalu:
Trace-Based Coinductive Operational Semantics for While. 375-390
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/OwensSS09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/OwensSS09
Scott Owens, Susmit Sarkar, Peter Sewell:
A Better x86 Memory Model: x86-TSO. 391-407
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/JulienP09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/JulienP09
Nicolas Julien, Ioana Pasca:
Formal Verification of Exact Computations Using Newton's Method. 408-423
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/SchimpfMS09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/SchimpfMS09
Alexander Schimpf, Stephan Merz, Jan-Georg Smaus:
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. 424-439
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Swierstra09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Swierstra09
Wouter Swierstra:
A Hoare Logic for the State Monad. 440-451
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/ThiemannS09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/ThiemannS09
René Thiemann, Christian Sternagel:
Certification of Termination Proofs Using CeTA. 452-468
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/Tuerk09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/Tuerk09
Thomas Tuerk:
A Formalisation of Smallfoot in HOL. 469-484
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/WangYZ09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/WangYZ09
Jinshuang Wang, Huabing Yang, Xingyuan Zhang:
Liveness Reasoning with Isabelle/HOL. 485-499
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/WinwoodKSACN09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/WinwoodKSACN09
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish:
Mind the Gap. 500-515

maintained by

, founded at