TPHOLs'99: Preliminary Program
- 11:00 Invited talk:
Thomas Kropf (Universität Tübingen)
Recent Advancements in Hardware Verification - How to make theorem
proving fit for an industrial usage
12:00 Lunch
- 13:20 Disjoint Sums over Type classes in HOL
Norbert Völker (University of Essex)
- 14:00
Inductive datatypes in HOL - lessons learned in Formal-Logic Engineering
Stefan Berghofer and Markus Wenzel (Technical University of Munich)
- 14:40
Isomorphisms - A Link Between the Shallow and the Deep
Thomas Santen (Technical University of Berlin)
15:20 Coffee Break
- 15:50
Polytypic Proof Construction
Holger Pfeifer and Harald Rueß (University of Ulm and SRI International)
- 16:30 Recursive Function Definition over Coinductive Types
John Matthews (Oregon Graduate Institute)
- 17:10 Hardware Verification using Co-induction in Coq
Solange Coupet-Grimal and Line Jakubiec (University of Marseille)
- 9:00 Invited talk:
Arjeh Cohen, (Technical University of Eindhoven).
Connecting Proof Checkers and Computer Algebra
using OpenMath
10:00 Coffee break
- 10:20
A machine-checked theory of floating point arithmetic
John R. Harrison (Intel)
- 11:00
Universal Algebra in Type Theory
Venanzio Capretta (University of Nijmegen)
- 11:40
Locales - A sectioning concept for Isabelle
Florian Kammüller, Markus Wenzel and Lawrence C. Paulson (Technical
University of Munich and University of Cambridge)
12:20 Lunch
- 13:30
Isar - a generic interpretative approach to readable formal proof documents
Markus Wenzel (Technical University of Munich)
- 14:10
On the Implementation of an Extensible Declarative Proof Language
Vincent Zammit (Sharp)
- 14:50
Three Tactic Theorem Proving
Don Syme (Microsoft Research Limited)
15:30 Coffee Break
Certification of Sorting Algorithms in the Coq System
Jean-Christophe Filliâtre and Nicolas Magaud (Université de Paris
Sud and Ecole Normale Supérieure de Lyon)
A case study in class library verification: Java's vector class
Marieke Huisman, Bart Jacobs, and Joachim van den Berg (University
of Nijmegen)
Embedding Algebraic Specifications in HOL
Dan Zhou and Shiu-Kai Chin (Florida Atlantic University and
Syracuse University)
- 9:00
Mechanized Operational Semantics via (Co)Induction
Simon J. Ambler and Roy L. Crole (Leicester University)
- 9:40
Representing WP Semantics in Isabelle/ZF
Mark Staples (University of Cambridge)
10:20 Coffee break
- 11:00
A HOL Conversion for Translating Linear Time Temporal Logic to
Omega-automata
Klaus Schneider and Dirk W. Hoffmann (University of Karlsruhe)
- 11:40
From I/O Automata to timed I/O automata
Bernd Grobauer and Olaf Müller (University of Aarhus and Technical
University of Munich)
12:20 Lunch
Thrusday afternoon
Excursion to Gourdon
Thursday evening
Banquet "Moulin des Moines" (Valbonne)
- 9:00 Invited talk:
Dominique Bolignano (Trusted Logic)
Formal Methods and Security Evaluation
10:00 Coffee break
- 10:30
Importing MDG Results into HOL
Haiyan Xiong, Paul Curzon, Sofiène Tahar (Midlesex University and
Concordia University)
- 11:10
Integrating Gandalf and HOL
Joe Hurd (University of Cambridge)
12:00 Lunch
- 13:00
Lifted-FL: A pragmatic Implementation of Combined Model Checking and Theorem Proving
Mark D. Aagaard, Robert B. Jones and Carl-Johan H. Seger (Intel)
- 13:40
Symbolic Functional Evaluation,
Nancy A. Day and Jeffrey J. Joyce (Oregon Graduate Institute and
Intrepid Critical Software Inc.)
Implementing Extensible Theorem Provers
Kathi Fisler, Shriram Krishnamurthi, and Kathryn E. Gray (Rice
University)
Importing Isabelle Formal Mathematics into NuPRL
Pavel Naumov (Cornell University)
Working with Linear Logic in Coq
James Power and Caroline Webster (National University of Ireland)
15:20 Coffee Break
Comments and Feedback:
TPHOLs99@sophia.inria.fr
Author: The TPHOLs'99 Organising Committee
Date Last Modified: Wed 31 May 2000
URL: schedule.html