[TYPES] TPHOLs: Call for participation

[slind at cs.utah.edu]

      [We apologize if you receive multiple copies of this message]


                  CALL FOR PARTICIPATION: TPHOLs 2004

                 The 17th International Conference on
                Theorem Proving in Higher Order Logics

                           Park City, Utah

              Tuesday 14 September - Friday 17 September 2004

              ***********************************************
              *     http://www.cs.utah.edu/tphols2004/      *
              ***********************************************

The 2004 International Conference on Theorem Proving in Higher Order
Logics will be the seventeenth in a series that dates back to 1988.
The conference will be held Tuesday September 14 through Friday
September 17 in Park City, Utah.


ACCEPTED PAPERS

    * Behzad Akbarpour and Sofiene Tahar
      Error Analysis of Digital Filters using Theorem Proving

    * Penny Anderson and Frank Pfenning
      Verifying Uniqueness in a Logical Framework

    * David Aspinall, Lennart Beringer, Martin Hofmann,
      Hans-Wolfgang Loidl, and Alberto Momigliano
      A Program Logic for Resource Verification

    * Olivier Boite
      Proof Reuse with Extended Inductive Types

    * Luis Cruz-Filipe and Freek Wiedijk
      Hierarchical Reflection

    * Lucas Dixon and Jacques Fleuriot
      Higher Order Rippling in IsaPlanner

    * Gamboa and John Cowles
      A Mechanical Proof of the Cook-Levin Theorem

    * Nadeem Abdul Hamid and Zhong Shao
      Interfacing Hoare Logic and Type Systems for Foundational
      Proof-Carrying Code

    * Jason Hickey and Aleksey Nogin
      Extensible Hierarchical Tactic Construction in a Logical Framework

    * Einar Broch Johnsen and Christoph Lueth
      Theorem Reuse by Proof Term Transformation
    * Michael Jones, Aaron Benson, and Dan Delorey
      Proving Compatibility using Refinement

    * Hanbing Liu and J Moore
      Java Program Verification via a JVM Deep Embedding in ACL2

    * John Longley and Randy Pollack
      Reasoning About CBV Functional Programs in Isabelle/HOL

    * Jean-Francois Monin
      Proof Pearl: From concrete to functional unparsing

    * Julien Narboux
      A Decision Procedure for Geometry in Coq

    * Michael Norrish
      Recursive function definition for types with binders

    * Lee Pike, Jeffrey Maddalon, Paul Miner, and Alfons Geser
      Abstractions for Fault-Tolerant Distributed System Verification

    * Stefan Richter
      Formalizing Integration Theory, with an Application to
      Probabilistic Algorithms

    * Martin Wildmoser and Tobias Nipkow
      Certifying machine code safety: shallow versus deep embedding

    * Ting Zhang, Henny B. Sipma, and Zohar Manna
      Term Algebras with Length Function and Bounded Quantifier
      Alternation

    * Zuo Tian-Jun, Han Jun-Gang, and Chen Ping
      Formalizing Java Dynamic Loading in HOL


INVITED SPEAKERS

 The following distinguished researchers will give talks at TPHOLs2004:

    * Al Davis, School of Computing, University of Utah
    * Tom Hales, Department of Mathematics, University of Pittsburgh
    * Ken McMillan, Cadence Berkeley Labs


REGISTRATION AND ACCOMODATION

Registration is now open. Please visit the TPHOLs 2004 website,

    http://www.cs.utah.edu/tphols2004/

to register and book hotel rooms. Early registration is 300 USD for
regular participants, 200 USD for students. The early registration
deadline is August 20, 2004.

The conference hotel is the Park City Marriott. The conference rate is
USD 79 per night + tax. Hotel bookings must be made by August 13, 2004
in order to guarantee availability and rate.


RELATED EVENTS

 There will be a gap of one day between the end of TPHOLs2004 and the
start of ICFP, the International Conference on Functional Programming.
ICFP will be held at Snowbird, Utah during Sept. 19-22. See
http://www.cs.indiana.edu/icfp04/cfp/cfp.html for details.


GETTING IN TOUCH

 Please use the address tphols2004 at cs.utah.edu if you wish to send
email to the organizers.