[isabelle] TPHOLs 2005 Final Call for Participation



              TPHOLs 2005 - FINAL CALL FOR PARTICIPATION

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

                             Oxford, UK
              Monday 22nd - Thursday 25th August 2005

            ********************************************
            *  http://web.comlab.ox.ac.uk/TPHOLs2005/  *
            ********************************************

The 2005 International Conference on Theorem Proving in Higher Order
Logics will be the eighteenth in a series that dates back to 1988.
The conference will be held Monday 22nd August through Thursday
25th August in central Oxford, UK.

REGISTRATION

Registration is now open.  Please visit the TPHOLs 2005 web site,
http://web.comlab.ox.ac.uk/TPHOLs2005/, to register.

INVITED SPEAKERS

Wolfgang Paul, Universitat des Saarlandes
     On the Correctness of Operating System Kernels

Andrew Pitts, University of Cambridge
     Alpha-Structural Recursion and Induction

ACCOMMODATION

Information on accommodation is available on the TPHOLs 2005 web site.

RELATED EVENTS

On Friday 26 August, the day after TPHOLs 2005 finishes, the NETCA
Workshop on Verification and Theorem Proving for Continuous Systems
will take place in Oxford. Further information on the NETCA workshop
can be found at http://www.dcs.qmul.ac.uk/~pbo/NETCA-workshop.html

SPONSORS

TPHOLs 2005 is sponsored by the following organizations:

 o Intel
 o NETCA
 o EPSRC

CONTACT

Enquiries concerning the conference should be emailed to
tphols2005 at comlab.ox.ac.uk

OUTLINE PROGRAMME

Monday 22nd, Tuesday 23rd: Technical sessions.

Wednesday 24th: Technical sessions; excursion; conference dinner.

Thursday 25th: Technical sessions.

ACCEPTED REGULAR PAPERS

Shallow Lazy Proofs
  Hasan Amjad

Mechanized Metatheory for the Masses: The PoplMark Challenge
  Brian Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster,
  Benjamin Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn,
  Stephanie Weirich and Steve Zdancewic

A Structured Set of Higher-Order Problems
  Christoph Benzmüller and Chad Brown

Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS
  Nestor Catano

Proving Equalities in a Commutative Ring Done Right in Coq
  Benjamin Grégoire and Assia Mahboubi

A HOL theory of Euclidean space
  John Harrison

A Design Structure for Higher Order Quotients
  Peter Homeier

Axiomatic Constructor Classes in Isabelle/HOLCF
  Brian Huffman, John Matthews and Peter White

Meta Reasoning in ACL2
  Warren Hunt, Matt Kaufmann, Robert Krug, J Moore and Eric Smith

Reasoning on Java programs with aliasing and frame conditions
  Claude Marche and Christine Paulin-Mohring

Real Number Calculations and Theorem Proving
  Cesar Munoz and David Lester

Verifying a Secure Information Flow Analyzer
  David Naumann

Proving Bounds for Real Linear Programs in Isabelle/HOL
  Steven Obua

Essential Incompleteness of Arithmetic Verified by Coq
  Russell O'Connor

Verification of BDD Normalization
  Veronika Ortner and Norbert Schirmer

Extensionality in the Calculus of Constructions
  Nicolas Oury

A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic
  Tom Ridge and James Margetson

A Generic Network on Chip Model
  Julien Schmaltz and Dominique Borrione

Formal Verification of a SHA-1 Circuit Core using ACL2
  Diana Toma and Dominique Borrione

>From PSL to LTL: A Formal Validation in HOL
  Thomas Türk and Klaus Schneider

ACCEPTED PROOF PEARLS

Proof Pearl: A Formal Proof of Higman's Lemma in ACL2
  Francisco-Jesús Martín-Mateos, Jose-Antonio Alonso,
  María-José Hidalgo and José-Luis Ruiz-Reina

Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2
  J Moore and Qiang Zhang

Proof Pearl: Defining Functions Over Finite Sets
  Tobias Nipkow and Lawrence Paulson

Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof
  Michael Norrish and Konrad Slind





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.