Email Gateway (Aug 18 2022 at 13:39): Email Gateway (Aug 18 2022 at 13:39):From: Stefan Berghofer <berghofe@in.tum.de>
TPHOLs 2009 - SECOND CALL FOR PARTICIPATION
The 22nd International Conference on
Theorem Proving in Higher Order Logics
Munich, Germany
Monday 17th - Thursday 20th August 2009
************
* http://tphols.in.tum.de * ************
TPHOLs is the premier international conference for researchers from all
areas of interactive theorem proving and its applications.
REGISTRATION
** Early registration deadline: 5 JULY 2009 (23:59 CEST, next Sunday!) **
Early registration fee (up to 5 July 2009): EUR 350 (students: EUR 245)
Late registration fee (from 6 July 2009): EUR 455 (students: EUR 320)
Please register at http://tphols.in.tum.de/fee.html
ACCOMMODATION
** Deadline for booking conference hotel at special rate of EUR 119: 5 JULY 2009 **
25 of the allocated rooms are still available until 26 JULY 2009
Reservations received after this date will be accepted on a space and
rate availability basis.
For information on hotel booking, see http://tphols.in.tum.de/hotel.html
SPONSORS
TPHOLs 2009 is sponsored by
o Microsoft Research Redmond
o Galois
o Verisoft XT
o Validas AG
o DFG doctorate programme Puma
o Siemens
CONTACT
tphols at in tum de
PRELIMINARY PROGRAMME
Pre-Conference Workshop (August 13-15)
Isabelle Developers Workshop http://tphols.in.tum.de/idw.html
Monday, August 17
08:00-09:00 REGISTRATION
09:00-10:00 INVITED TALK 1
David Basin. Let's Get Physical: Models and Methods for Real-World Security Protocols
10:00-10:30 COFFEE
10:30-12:10 SESSION 1
Assia Mahboubi, Georges Gonthier, Laurence Rideau and François Garillot.
Packaging Mathematical Structures
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen and Enrico Tassi.
Hints in unification
Ioana Pasca and Nicolas Julien.
Formal verification of exact computations using Newton's method
Osman Hasan, Sanaz Khan Afshar and Sofiene Tahar.
Formal Analysis of Optical Waveguides in HOL
12:10-13:40 LUNCH
13:40-15:20 SESSION 2
Wouter Swierstra. Proof pearl: The Hoare State Monad
Keiko Nakata and Tarmo Uustalu. Trace-based coinductive operational semantics for While:
Big-step and small-step, functional and relational styles
Andreas Lochbihler. Formalising FinFuns -
Generating Code for Functions as Data from Isabelle/HOL
Stephane Le Roux. Acyclic preferences and existence of sequential Nash equilibria:
a formal and constructive equivalence
15:20-15:50 COFFEE
15:50-17:30 SESSION 3
Jesper Bengtson and Joachim Parrow. Psi-calculi in Isabelle
Jeremy E. Dawson and Alwen Tiu.
Formalising Observer Theory for Environment-Sensitive Bisimulation
Brian Huffman. A Purely Definitional Universal Domain
Nick Benton, Andrew Kennedy and Carsten Varming.
Some Domain Theory and Denotational Semantics in Coq
Tuesday, August 18
08:00-09:00 INVITED TUTORIAL 1
John Harrison. HOL Light: an overview
09:00-10:00 INVITED TALK 2
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen,
Wolfram Schulte and Stephan Tobies. VCC: A Practical System for Verifying Concurrent C
10:00-10:30 COFFEE
10:30-12:10 SESSION 4
Rene Thiemann and Christian Sternagel. Certification of Termination Proofs using CeTA
Jinshuang Wang, Xingyuan Zhang and Huabing Yang. Liveness Reasoning with Isabelle/HOL/Isar
Dabrowski Frederic and David Pichardie. A Certified Data Race Analysis for a Java-like Language
Stefan Berghofer, Lukas Bulwahn and Florian Haftmann.
Turning inductive into equational specifications
12:10-13:40 LUNCH
13:40-15:20 POSTER SESSION
15:20-16:00 COFFEE
16:00-17:00 BUSINESS MEETING
Wednesday, August 19
08:00-09:00 INVITED TUTORIAL 2
Adam Naumowicz. A Brief Overview of Mizar
09:00-10:00 INVITED TALK 3
John Harrison. Without Loss of Generality
10:00-10:30 COFFEE
10:30-11:45 SESSION 5
Rafal Kolanski and Gerwin Klein. Types, Maps and Separation Logic
Andrew McCreight. Practical Tactics for Separation Logic
Thomas Tuerk. A Formalisation of Smallfoot in HOL
11:45-13:00 LUNCH
13:00-23:00 EXCURSION
Thursday, August 20
08:00-09:00 INVITED TUTORIAL 3
Ana Bove, Ulf Norell and Peter Dybjer.
A Brief Overview of Agda - A Functional Language with Dependent Types
09:00-10:00 INVITED TUTORIAL 4
Carsten Schürmann. The Twelf Proof Assistant
10:00-10:30 COFFEE
10:30-12:10 SESSION 6
Scott Owens, Susmit Sarkar and Peter Sewell. A better x86 memory model: x86-TSO
Magnus O. Myreen and Mike Gordon. Verified LISP implementations on ARM, x86 and PowerPC
Javier de Dios and Ricardo Pena.
Formal Certification of a Resource-Aware Language Implementation
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish.
Mind the Gap: A Verification Framework for Low-Level C
12:10-13:40 LUNCH
13:40-15:20 SESSION 7
Peter Homeier. The HOL-Omega Logic
Chad Brown and Gert Smolka. Extended First-Order Logic
Alexander Schimpf, Stephan Merz and Jan-Georg Smaus.
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
Stefan Berghofer and Markus Reiter. Formalizing the Logic-Automaton Connection
15:20-15:50 COFFEE
Post-Conference Workshops (Friday, August 21)
PLMMS http://plmms09.cse.tamu.edu/
Coq Workshop http://coq.inria.fr/coq-workshop/
Last updated: May 03 2024 at 08:18 UTC