[TYPES/announce] TPHOLs 2009 in Munich: Call for Participation and Accepted Papers

[Stefan Berghofer]

NOTE: THE EARLY (DISCOUNT) REGISTRATION DEADLINE IS 5 JULY 2009


                TPHOLs 2009 - 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 and ACCOMMODATION

 http://tphols.in.tum.de/index.html#registration

 The reduced registration fee is available up to and including 5 July 2009.

INVITED SPEAKERS

 David Basin      ETH Zürich, Switzerland
 John Harrison    Intel, USA
 Wolfram Schulte  Microsoft Research, USA

INVITED TUTORIALS

 Agda       Ulf Norell
 HOL Light  John Harrison
 Mizar      Adam Naumowicz
 Twelf      Carsten Schürmann

RELATED EVENTS

 This year, the workshop on Programming Languages for Mechanized
 Mathematics Systems (PLMMS 2009), and the Coq workshop, both on
 Friday 21 August, are co-located with the conference. In addition,
 the Isabelle Developers Workshop will take place on 13 - 15 August
 just before the conference.

 Further information about the workshops can be found at

 http://plmms09.cse.tamu.edu/
 http://coq.inria.fr/coq-workshop/
 http://tphols.in.tum.de/idw.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

OUTLINE PROGRAMME

 Conference:

 Monday 17th:    Technical sessions
 Tuesday 18th:   Technical sessions.
 Wednesday 19th: Technical sessions, excursion and conference dinner.
 Thursday 20th:  Technical sessions.

 Workshops

 Thursday 13th - Saturday 15th: Isabelle Developers Workshop
 Friday 21st: PLMMS 2009 and Coq workshops.

CONTACT

 tphols at in tum de

ACCEPTED PAPERS

Andreas Lochbihler.
  Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL

Alwen Tiu and Jeremy E. Dawson.
  Formalising Observer Theory for Environment-Sensitive Bisimulation

Stefan Berghofer and Markus Reiter.
  Formalizing the Logic-Automaton Connection

Stefan Berghofer, Lukas Bulwahn and Florian Haftmann.
  Turning inductive into equational specifications

Chad Brown and Gert Smolka.
  Extended First-Order Logic

Magnus O. Myreen and Mike Gordon.
  Verified LISP implementations on ARM, x86 and PowerPC

Brian Huffman.
  A Purely Definitional Universal Domain

Peter Homeier.
  The HOL-Omega Logic

Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish.
  Mind the Gap: A Verification Framework for Low-Level C

Alexander Schimpf, Stephan Merz and Jan-Georg Smaus.
  Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL

René Thiemann and Christian Sternagel.
  Certification of Termination Proofs using CeTA

Stephane Le Roux.
  Acyclic preferences and existence of sequential Nash equilibria: a formal
  and constructive equivalence

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen and Enrico Tassi.
  Hints in unification

Javier de Dios and Ricardo Pena.
  Formal Certification of a Resource-Aware Language Implementation

Dabrowski Frédéric and David Pichardie.
  A Certified Data Race Analysis for a Java-like Language

Wouter Swierstra.
  Proof pearl: The Hoare State Monad

François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau.
  Packaging Mathematical Structures

Nick Benton, Andrew Kennedy and Carsten Varming.
  Some Domain Theory and Denotational Semantics in Coq

Thomas Tuerk.
  A Formalisation of Smallfoot in HOL

Rafal Kolanski and Gerwin Klein.
  Types, Maps and Separation Logic

Jesper Bengtson and Joachim Parrow.
  Psi-calculi in Isabelle

Ioana Pasca and Nicolas Julien.
  Formal verification of exact computations using Newton's method

Scott Owens, Susmit Sarkar and Peter Sewell.
  A better x86 memory model: x86-TSO

Andrew McCreight.
  Practical Tactics for Separation Logic

Osman Hasan, Sanaz Khan Afshar and Sofiene Tahar.
  Formal Analysis of Optical Waveguides in HOL