[Om-announce] LAST CALL FOR PARTICIPATION (TPHOLs'2008)

[Otmane Ait Mohamed]

                LAST CALL FOR PARTICIPATION


21st International Conference on Theorem Proving in
              Higher Order Logics
                (TPHOLs 2008)

      http://www.ece.concordia.ca/TPHOLs2008
           tphols08 at ece.concordia.ca

    August 18-21, 2008, Montreal, Quebec, Canada


The 2008 International Conference on Theorem Proving in Higher Order
Logics will be the 21st in a series that dates back to 1988. The
conference will be held in Montreal, Quebec, Canada, on 18-21 August 2008.


REGISTRATION

Registration is now open.  Please visit the TPHOLs 2008 web site,
http://www.ece.concordia.ca/TPHOLs2008/, to register.

INVITED SPEAKERS

Mike Gordon, University of Cambridge, UK.

  Twenty Years of Theorem Proving for HOLs


Steve Miller, Advanced Technology Center, Rockwell Collins, USA

   Will This Be Formal?


INVITED TUTORIALS

   Konrad Slind. A Brief Overview of HOL4

   Sam Owre. A Brief Overview of PVS

   Makarius Wenzel. The Isabelle Framework

   Yves Bertot. A short presentation of Coq

   Matt Kaufmann. An ACL2 Tutorial


ACCOMMODATION

Information on accommodation is available on the TPHOLs 2008 web site
(click on the registration tab).


RELATED EVENTS

On Friday 22 August, the day after TPHOLs 2008 finishes, the UITP
Workshop on User Interfaces for Theorem Proving will take place.
Further information on the UITP workshop
can be found at http://www.informatik.uni-bremen.de/~cxl/uitp/

SPONSORS

TPHOLs 2008 is sponsored by the following organizations:

 o ENCS
 o NIA
 o Intel
 o RESMIQ
 o ConcordiA University


CONTACT

Inquiries concerning the conference should be emailed to
tphols08 at ece.concordia.ca


------------------------------------------------------------------------
OUTLINE PROGRAM

Monday 18th, Tuesday 19th: Technical sessions.

Wednesday 20th: Technical sessions; Museum Visit; conference dinner.

Thursday 21st: Technical sessions.

Friday 22nd : UITP workshop.

The final program is available on the conference web site.

VENUE

TPHOLs'08 will be be held at the new Concordia Engineering & Computer Science building,
home of the Engineering and Computer Science faculty.

--------------------------------------------------------------------------

ACCEPTED REGULAR PAPERS

Klaus Aehlig, Florian Haftmann and Tobias Nipkow. A Compiled
Implementation of Normalization by Evaluation

Daniel Wasserrab and Andreas Lochbihler. Formalizing a Framework for
Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL

Ana Bove and Venanzio Capretta. A Type of Partial Recursive Functions

Sascha Bhme, Rustan Leino and Burkhart Wolff. HOL-Boogie --- An
Interactive Prover for the Boogie Program-Verifier

Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkok and John
Matthews. Imperative Functional Programming with Isabelle/HOL

David Cock, Gerwin Klein and Thomas Sewell. Secure Microkernels, State
Monads and Scalable Refinement

David Lester. Real Number Calculations and Theorem Proving: Validation and
Use of an Exact Arithmetic

Holger Gast. Lightweight Separation

Hasan Amjad. LCF-style Propositional Simplification With BDDs and SAT
Solvers

Jens Brandt and Klaus Schneider. Formal Reasoning about Causality Analysis

Pierre Courtieu, Julien Forest and Xavier Urbain. Certifying a Termination
Criterion Based on Graphs, without Graphs

Matthieu Sozeau and Nicolas Oury. First-Class Type Classes

Yves Bertot, Georges Gonthier, Sidi Ould Biha and Ioana Pasca. Canonical
Big Operators

Stefan Berghofer and Christian Urban. Nominal Inversion Principles

Polyvios Pratikakis, Jeff Foster, Michael Hicks and Iulian Neamtiu.
Formalizing Soundness of Contextual Effects

Laurent Thery. Proof Pearl: Revisiting the Mini-Rubik in Coq

Russell O'Connor. Certified Exact Transcendental Real Number Computation
in Coq

Sayan Mitra and K. Mani Chandy. A Formalized Theory for Verifying
Stability and Convergence of Automata in PVS