TPHOLs

Keyphrases

Publications

2009

Andreas Lochbihler
Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs (2009)
Stefan Berghofer, Lukas Bulwahn, Florian Haftmann
Turning Inductive into Equational Specifications. TPHOLs (2009)
Stefan Berghofer, Markus Reiter
Formalizing the Logic-Automaton Connection. TPHOLs (2009)
David A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt
Let's Get Physical: Models and Methods for Real-World Security Protocols. TPHOLs (2009)
Jeremy E. Dawson, Alwen Tiu
Formalising Observer Theory for Environment-Sensitive Bisimulation. TPHOLs (2009)
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. TPHOLs (2009)
Frédéric Dabrowski, David Pichardie
A Certified Data Race Analysis for a Java-like Language. TPHOLs (2009)
Peter V. Homeier
The HOL-Omega Logic. TPHOLs (2009)
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish
Mind the Gap. TPHOLs (2009)
Keiko Nakata, Tarmo Uustalu
Trace-Based Coinductive Operational Semantics for While. TPHOLs (2009)
Ana Bove, Peter Dybjer, Ulf Norell
A Brief Overview of Agda - A Functional Language with Dependent Types. TPHOLs (2009)
Nick Benton, Andrew Kennedy, Carsten Varming
Some Domain Theory and Denotational Semantics in Coq. TPHOLs (2009)
Osman Hasan, Sanaz Khan Afshar, Sofiène Tahar
Formal Analysis of Optical Waveguides in HOL. TPHOLs (2009)
Magnus O. Myreen, Michael J. C. Gordon
Verified LISP Implementations on ARM, x86 and PowerPC. TPHOLs (2009)
Chad E. Brown, Gert Smolka
Extended First-Order Logic. TPHOLs (2009)
Thomas Tuerk
A Formalisation of Smallfoot in HOL. TPHOLs (2009)
Jesper Bengtson, Joachim Parrow
Psi-calculi in Isabelle. TPHOLs (2009)
Wouter Swierstra
A Hoare Logic for the State Monad. TPHOLs (2009)
François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
Packaging Mathematical Structures. TPHOLs (2009)
René Thiemann, Christian Sternagel
Certification of Termination Proofs Using CeTA. TPHOLs (2009)
Andrew McCreight
Practical Tactics for Separation Logic. TPHOLs (2009)
Javier de Dios, Ricardo Peña-Marí
Formal Certification of a Resource-Aware Language Implementation. TPHOLs (2009)
Scott Owens, Susmit Sarkar, Peter Sewell
A Better x86 Memory Model: x86-TSO. TPHOLs (2009)
Rafal Kolanski, Gerwin Klein
Types, Maps and Separation Logic. TPHOLs (2009)
John Harrison
HOL Light: An Overview. TPHOLs (2009)
Stéphane Le Roux
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence. TPHOLs (2009)
Alexander Schimpf, Stephan Merz, Jan-Georg Smaus
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. TPHOLs (2009)
John Harrison
Without Loss of Generality. TPHOLs (2009)
Adam Naumowicz, Artur Kornilowicz
A Brief Overview of Mizar. TPHOLs (2009)
Carsten Schürmann
The Twelf Proof Assistant. TPHOLs (2009)
Brian Huffman
A Purely Definitional Universal Domain. TPHOLs (2009)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
Hints in Unification. TPHOLs (2009)
Nicolas Julien, Ioana Pasca
Formal Verification of Exact Computations Using Newton's Method. TPHOLs (2009)
Jinshuang Wang, Huabing Yang, Xingyuan Zhang
Liveness Reasoning with Isabelle/HOL. TPHOLs (2009)

volume 5674, 2009

Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings TPHOLs 5674 (2009)

2008

volume 5170, 2008

Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings TPHOLs 5170 (2008)