Email Gateway (Aug 18 2022 at 13:29): Email Gateway (Aug 18 2022 at 13:29):From: Stefan Berghofer <berghofe@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC