[Prev][Next][Index][Thread]

TPHOLs 2001 Call For Participation


[ This conference may be of interest to TYPES readers; note that the
programme includes a number of papers with a type-theoretic
dimension. ]


                 TPHOLs 2001 - CALL FOR PARTICIPATION

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

                          Edinburgh, Scotland
              Monday 3rd  - Thursday 6th September 2001

              *****************************************
              *  http://www.dcs.gla.ac.uk/TPHOLs2001  *
              *****************************************

The 2001 International Conference on Theorem Proving in Higher Order
Logics will be the fourteenth in a series that dates back to 1988.
The conference will be held Monday 3rd September through Thursday 
6th September in central Edinburgh, Scotland. 

REGISTRATION

Registration is now open.  Please visit the TPHOLs 2001 web site,
http://www.dcs.gla.ac.uk/TPHOLs2001, to register. A reduced
registration fee is available when registering for both TPHOLs 2001
and CHARME 2001 (see below).

INVITED SPEAKERS

Bart Jacobs, University of Nijmegen 
     JavaCard Program Verification 

Steven D. Johnson, Indiana University 
     View from the Fringe of the Fringe
     (Joint with CHARME 2001) 

N. Shankar, SRI International 
     Using Decision Procedures with a Higher-Order Logic 

ACCOMMODATION

Information on accommodation is now available on the TPHOLs 2001 web
site.

STUDENT BURSARIES

A small number of bursaries will be made available to assist students
to attend TPHOLs 2001. More information about these will be made
available on the conference web site.

RELATED EVENTS

TPHOLs 2001 will be co-located with the 11th Advanced Research Working
Conference on Correct Hardware Design and Verification Methods (CHARME
2001), which will be held during 4 - 7 September 2001 in the nearby
town of Livingston.  A joint half-day session is planned for Wednesday
5th September.  Further information on CHARME 2001 is available at
http://www.dcs.gla.ac.uk/CHARME2001.

SPONSORS

TPHOLs 2001 is sponsored by the following organizations:

 o Intel
 o Microsoft Research

CONTACT

Enquiries concerning the conference should be emailed to
tphols2001@inf.ed.ac.uk.

OUTLINE PROGRAMME

Monday 3rd, Tuesday 4th: Technical sessions.

Wednesday 5th: Joint technical sessions with CHARME 2001; 
               excursion; conference dinner.

Thursday 6th: Technical sessions.

ACCEPTED FULL RESEARCH PAPERS

Computer Algebra Meets Automated Reasoning: 
  Integrating Maple and PVS 
     Andrew Adams, Martin Dunstan, Hanne Gottliebsen, 
     Tom Kelsey, Ursula Martin, Sam Owre 

An Irrational Construction of R from Z 
     R. D. Arthan 

HELM and the Semantic Math-Web 
     Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, 
     Irene Schena 

Calculational Reasoning Revisited - an Isabelle/Isar Experience 
     Gertrud Bauer, Markus Wenzel 

Mechanical Proofs about a Non-Repudiation Protocol 
     Giampaolo Bella, Larry Paulson 

Proving Hybrid Protocols Correct 
     Mark Bickford, Christoph Kreitz, Robbert van Renesse, 
     Xiaoming Lin 

Nested General Recursion and Partiality in Type Theory 
     Ana Bove, Venanzio Capretta 

A Higher-Order Calculus for Categories 
     Mario Cáccamo, Glynn Winskel 

Certifying the Fast Fourier Transform with Coq 
     Venanzio Capretta 

A Generic Library of Floating-Point Numbers and its 
  Application to Exact Computing 
     Marc Daumas, Laurence Rideau, Laurent Théry 

Abstraction and Refinement in Higher Order Logic 
     Matt Fairtlough, Michael Mendler, Xiaochun Cheng 

A Framework for the Formalisation of Pi Calculus 
  Type Systems in Isabelle/HOL 
     Simon Gay 

Statecharts Revisited 
     Steffen Helke, Florian Kammüller 

Refinement Calculus for Logic Programming in Isabelle/HOL 
     David Hemer, Ian Hayes, Paul Strooper 

Predicate Subtyping with Predicate Sets 
     Joe Hurd 

A Structural Embedding of Ocsid in PVS 
     Pertti Kellomäki 

A Certified Polynomial-Based Decision Procedure for 
  Propositional Logic 
     Inmaculada Medina-Bulo, Francisco Palomo-Lozano, 
     José A. Alonso-Jiménez 

Finite Set Theory in ACL2 
     J Strother Moore 

The HOL/NuPRL Proof Translator 
     Pavel Naumov, Mark-Oliver Stehr, José Meseguer 

Formalizing Convex Hulls Algorithms 
     David Pichardie, Yves Bertot 

Experiments with Finite Tree Automata in Coq 
     Xavier Rival, Jean Goubault-Larrecq 

Ordinal Arithmetic: A Case Study for Rippling in a 
  Higher Order Domain 
     Alan Smaill, Louise A. Dennis 

Mizar Light for HOL Light 
     Freek Wiedijk