[TYPES/announce] TPHOLs 2009: Early Registration Deadline Approaching (5th of July)

[Stefan Berghofer]

************************************************************************************
*  NOTE: THE EARLY (DISCOUNT) REGISTRATION DEADLINE IS 5 JULY 2009 (next Sunday!)  *
************************************************************************************


            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/