[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Sunday!)  *


                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.


 **** 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


 **** 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


 TPHOLs 2009 is sponsored by

  o Microsoft Research Redmond
  o Galois
  o Verisoft XT
  o Validas AG
  o DFG doctorate programme Puma
  o Siemens


 tphols at in tum de


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 
               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 
             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

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 
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/

Reply via email to