[Prev][Next][Index][Thread]
TPHOLs 2000: Call for Participation
-
To: acl2@lists.cc.utexas.edu, alp-diffusion@univ-lille1.fr, bra-types@cs.chalmers.se, coq-club@pauillac.inria.fr, elf-list@cs.cmu.edu, facs-members@lut.ac.uk, formal-methods@cs.uidaho.edu, imps@linus.mitre.org, info-hol@jaguar.cs.byu.edu, isabelle-users@cl.cam.ac.uk, lambda-usergroup@dcs.ed.ac.uk, lego-club@dcs.ed.ac.uk, logic@cs.stanford.edu, lprolog-list@cis.upenn.edu, nuprlnotes@www.cs.cornell.edu, procos-list@comlab.ox.ac.uk, pvs@csl.sri.com, qed@mcs.anl.gov, softverf@jaguar.cs.byu.edu, theorem-provers@ai.mit.edu, types@cis.upenn.edu
-
Subject: TPHOLs 2000: Call for Participation
-
From: Mark Aagaard <maagaard@ichips.intel.com>
-
Date: Fri, 19 May 2000 16:15:59 -0700
CALL FOR PARTICIPATION: TPHOLs 2000
The 13th International Conference on
Theorem Proving in Higher Order Logics
Portland, Oregon, USA
Monday 14 August - Friday 18 August 2000
***************************************
* http://www.cse.ogi.edu/tphols2000 *
***************************************
The 2000 International Conference on Theorem Proving in Higher Order
Logics will be the thirteenth in a series that dates back to 1988.
The conference will be held Monday 14 August through Friday 18 August,
2000, at the DoubleTree Hotel, Portland, Oregon, USA. The first day
of the conference will be devoted to tutorials, with the remaining 4
days covering the main conference program.
Deadline for early registration: 30 June 2000
http://www.cse.ogi.edu/tphols2000/registration.htm
Deadline for hotel registration: 21 July 2000
http://www.cse.ogi.edu/tphols2000/hotelinfo.htm
With a record number of submissions spanning theory and applications,
a special tutorials day covering both introductory and advanced
topics, and an excellent set of invited talks, we expect this to be a
very stimulating and fun conference. Portland is a vibrant city of
coffee houses, restaurants, brew pubs, parks, bookstores, and bike
paths located at the fork of the Willamette and Columbia rivers in the
US Pacific Northwest.
We hope to see you in August!
Mark Aagaard, TPHOLs 2000 Organizing Committee
(tphols2000@cse.ogi.edu)
+------------------------------------------------------------------------
| Tutorial Day
+------------------------------------------------------------------------
Mon, Aug 14, 2000
TUTORIAL SESSION 1:
Introduction to Higher-Order Logic Theorem Proving
Perry Alexander, Kansas State University
TUTORIAL SESSION 2:
Principles and Practice of Symbolic Trajectory Evaluation
Andrew Martin, Motorola
TUTORIAL SESSION 3a:
Type theory and inductive reasoning using Coq
Yves Bertot, INRIA
TUTORIAL SESSION 3b:
Overview of ACL2
J Strother Moore, University of Texas at Austin
+------------------------------------------------------------------------
| Conference
+------------------------------------------------------------------------
Tue, Aug 15, 2000
INVITED TALK: Bob Colwell, Intel Corporation
SESSION 1: INDUSTRIAL VERIFICATION (I)
Victor Carreno and Cesar Munoz
Aircraft Trajectory Modeling and Alerting Algorithm Verification
Jim Grundy
Verified Optimizations for the Intel IA-64 Architecture
Roope Kaivola and Mark Aagaard
Divider circuit verification with model checking and theorem proving
SESSION 2: REFLECTION AND PROOF MANIPULATION
Stefan Berghofer and Tobias Nipkow
Proof terms for simply typed higher order logic
Ewen Denney
A Prototype Proof Translator from HOL to Coq
Herman Geuvers, Freek Wiedjik and Jan Zwanenburg
Equational Reasoning via Partial Reflection
SESSION 3: IMPLEMENTATION
Bruno Barras
Programming and Computing in HOL
Christoph Lueth and Burkhart Wolff
TAS -- A Generic Window Inference System
Jason Hickey and Aleksey Nogin
Fast Tactic-based Theorem Proving
POSTER SESSION 1
------------------------------------------------------------------------
Wed, Aug 16, 2000
SESSION 4: COMBINING THEOREM PROVING AND MODEL CHECKING
Karthikeyan Bhargavan, Carl Gunther, and Davor Obradovic
Routing Information Protocol in HOL/SPIN
Mike Gordon
Reachability programming in Hol98 using BDDs
SESSION 5: INDUSTRIAL VERIFICATION (II)
John Harrison
Formal Verification of IA-64 Division Algorithms
Mickael Kerboeuf, David Nowak, and Jean-Pierre Talpin
Specification and Verification of a Steam-Boiler with Signal-Coq
Abdel Mokkedem and Tim Leonard
Formal verification of the Alpha 21364 network protocol
EXCURSION: Mt Hood Railroad
------------------------------------------------------------------------
Thu, Aug 17, 2000
INVITED TALK: Larry Wos, Argonne National Laboratory
SESSION 6: FORMALIZED MATHEMATICS
Jacques D. Fleuriot
On the Mechanization of Real Analysis in Isabelle/HOL
Hanne Gottliebsen
Transcendental Functions and Continuity Checking in PVS
M. Randall Holmes
A Strong and Mechanizable Grand Logic
SESSION 7: ALGORITHM VERIFICATION
Catherine Dubois
Typing Soundness of ML within Coq
Stephan Merz
Complementation of Weak Alternating Automata in Isabelle/HOL
Pierre Letouzey and Laurent Thery
Formalizing Stalmarck's algorithm in Coq
SESSION 8: TYPE THEORY
Antonio Balaa and Yves Bertot
Fix-point Equations for Well-founded recursion in Type Theory
Venanzio Capretta
Recursive Families of Inductive Types
Randy Pollack
Dependently Typed Records for Representing Mathematical Structure
POSTER SESSION 2
------------------------------------------------------------------------
Fri, Aug 18, 2000
INVITED TALK: Robin Milner, Cambridge University
SESSION 9: THEORY OF PROGRAM VERIFICATION
Paul Jackson
Total-Correctness Refinement for Sequential Reactive Systems
Konrad Slind
Another Look at Nested Recursion
Linas Laibinis and Joakim von Wright
Functional Procedures in Higher-Order Logic
SESSION 10: MODELING OBJECT-ORIENTATION
Marieke Huisman and Bart Jacobs
Inheritance in Higher Order Logic: Modeling and Reasoning
Bernhard Reus and Tatjana Hein
Towards a Machine-Checked Java Specification Book
Martin Hofmann and Francis Tang
Implementing a Program Logic of Objects in a Higher-Order
Logic Theorem Prover
BUSINESS MEETING