TPHOLs'98: Draft Schedule

Contents

• TPHOLs'98 and IRW/FMP'98 Schedule
• TPHOLs'98 Papers

TPHOLs'98 and IRW/FMP'98 Schedule

A welcome BBQ for TPHOLs'98 participants will be held on the evening of Sunday 27 September at Burgmann College.

A welcome BBQ for IRW/FMP'98 participants will be held on the evening of Monday 28 September at Burgmann College.

TPHOLs'98 commences with registration at 9am on Monday 28 September, and concludes at 3:30pm on Thursday 1 October.

For participants in both TPHOLs'98 and IRW/FMP'98, the commencement is registration at 9am on Monday 28 September, and the conclusion is 3:30pm on Friday 2 October.

The joint TPHOLs'98 and IRW/FMP'98 dinner will be held on the evening of Tuesday 29 September.

Draft Timetable

The timetable below incorporates both TPHOLs'98 and IRW/FMP'98.

Invited speakers have 50 minutes plus 10 minutes for questions.
Speakers for refereed papers have 25 minutes plus 5 minutes for questions.
IRW/FMP Work-in-Progress speakers have 15 minutes plus 5 minutes for questions.
TPHOLs Work-in-Progress speakers have 10 minutes, and the opportunity for discussion of their work during the poster display.

Refreshments are in the Robertson Theatre foyer.

Sessions

Note: papers are denoted in the following manner:

• Invited Paper
• Refereed Paper
• Work in Progress Paper

Session A: Monday 1000

TPHOLs'98 Poster Session
Robertson Theatre

10 minute talks, followed by poster displays.

• Embedding a Formal Notation: Experiences of Automating the Embedding of Z in the Higher Order Logics of PVS and HOL
  Andrew M. Gravell and Chris H. Pratten
  University of Southampton, United Kingdom
  
  
• Requirements for a Simple Proof Checker
  Geoffrey Watson
  University of Queensland, Australia
  
  
• Some Theorem Proving Aids
  Paul E. Black¹ and Phillip J. Windley^{2
  1}National Institute of Standards and Technology
  ²Brigham Young University
  
  
• Verification of the MDG Components Library in HOL
  Paul Curzon,¹ Sofiène Tahar,² and Otmane Aït Mohamed^{3
  1}Middlesex University, United Kingdom
  ²Concordia University, Canada
  ³University of Montreal, Canada
  
  
• Building HOL90 Everywhere Easily (Well Almost)
  Elsa L. Gunter
  Bell Laboratories, United States
  
  
• Simulating Term-Rewriting in LPF and in Display Logic
  Jeremy E. Dawson
  The Australian National University, Australia

Session B: Monday 1200

TPHOLs
Robertson Theatre

• Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling
  François Puitg and Jean-François Dufourd
  LSIIT, France
  
  
• Formalization of Graph Search Algorithms and Its Applications
  Mitsuharu Yamamoto,¹ Koichi Takahashi,² Masami Hagiya,² Shim-ya Nishizaki,¹ and Tetsuo Tamai^{2
  1}Chiba University, Japan
  ²University of Tokyo, Japan
  
  

Session C: Monday 1430

TPHOLs
Robertson Theatre

• A Tool for Data Refinement
  Rimvydas Ruksenas and Joakim von Wright
  Åbo Akademi University, Finland
  
  
• Formalizing Dijkstra
  John Harrison
  Intel
  
  

Session D: Monday 1600

TPHOLs
Robertson Theatre

• Object-Oriented Verification based on Record Subtyping in Higher-Order Logic
  Wolfgang Narashewski and Markus Wenzel
  Technische Universität München, Germany
  
  
• The Village Telephone System: A Case Study in Formal Software Engineering
  Karthikeyan Bhargavan,¹ Carl Gunter,¹ Elsa Gunter,² Michael Jackson,³ Davor Obradovic,¹ and Pamela Zave^{3
  1}University of Pennsylvania, United States
  ²Bell Labs, United States
  ³AT&T Labs, United States
  
  
• Verifying a Garbage Collection Algorithm
  Paul Jackson
  University of Edinburgh, United Kingdom
  
  

Session E: Tuesday 0830

TPHOLs
Forestry Theatre

• Mechanical Verification of Total Correctness Through Diversion Verification Conditions
  Peter Homeier and David Martin
  University of Pennsylvania, United States
  
  
• Generating Embeddings from Denotational Descriptions
  Richard Boulton
  University of Edinburgh, United Kingdom
  
  

Session F: Tuesday 1000

Session G: Tuesday 1200

Joint TPHOLs and IRW/FMP Invited Paper
Robertson Theatre

• Extending Window Inference
  Joakim von Wright
  Åbo Akademi University, Finland

Session H: Tuesday 1430

IRW/FMP
Forestry Theatre

• Towards Verification of Non-repudiation Protocols
  Jianying Zhou¹ and Dieter Gollmann^{2
  1}National University of Singapore, Singapore
  ²Microsoft Research Limited, United Kingdom
  
  
• Security Management Via Z and CSP
  Andrew Simpson, Jim Davies, and Jim Woodcock
  Oxford University, United Kingdom
  

Session I: Tuesday 1600

IRW/FMP
Robertson Theatre

• Refinement of Z Machines
  Karl Lermer
  University of Queensland, Australia
  
  
• A Mode System for Flexible Alias Protection
  John Potter, David Clarke, and James Noble
  Microsoft Research Institute, Australia
  
  
• Local Stores in C++
  Mark Utting and James Dunwoody
  University of Waikato, New Zealand
  

Session J: Wednesday 0830

Joint TPHOLs and IRW/FMP Session
TPHOLs Invited Paper
Robertson Theatre

• Verified Lexical Analysis
  Tobias Nipkow
  Technische Universität München, Germany
  

Session K: Wednesday 1000

Session L: Wednesday 1200

Session M: Wednesday 1430

TPHOLs
Robertson Theatre

• A Comparison of PVS and Isabelle-HOL
  David Griffioen,¹ and Marieke Huisman^{2
  1}CWI, The Netherlands
  ²University Nijmegen, The Netherlands
  
  
• A Type Annotation Scheme for Nuprl
  Douglas Howe
  Bell Labs, United States

Session N: Wednesday 1600

TPHOLs
Robertson Theatre

• Program Abstraction in a Higher Order Logic Framework
  Marco Benini, Sara Kalvala, and Dirk Nowotka
  University of Warwick, UK
  
  
• On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System
  Naren Narasimhan and Ranga Vemuri
  University of Cincinnati, United States
  
  
• Co-Inductive Axiomatization of a Synchronous Language
  David Nowak, Jean-René Beauvais, and Jean-Pierre Talpin
  IRISA, France

Session O: Thursday 0830

Joint TPHOLs and IRW/FMP Session
IRW/FMP Invited Paper
Robertson Theatre

• Industrial-strength Refinement
  Jim Woodcock
  Oxford University, United Kingdom

Session P: Thursday 1000

Session Q: Thursday 1200

Session R: Thursday 1430

Session S: Thursday 1600

IRW/FMP
Robertson Theatre

• What's in a Specification?
  Linas Laibinis and Joakim von Wright
  Åbo Akademi University, Finland
  
  
• New Foundations for Z
  Martin Henson¹ and Steve Reeves^{2
  1}University of Essex, United Kingdom
  ²University of Waikato, New Zealand
  
  
• Tail-recursive Non-canonical Constants and Continuations in Martin-Löf's Type Theory
  Neil Leslie
  Massey University at Albany, New Zealand

Session T: Friday 0830

IRW/FMP Invited Paper
Robertson Theatre

• Separating Timing and Calculation in Real-Time Refinement
  Ian Hayes
  University of Queensland, Australia

Session U: Friday 1000

IRW/FMP
Robertson Theatre

• Issues for a Temporal Refinement Calculus
  Ron van der Meyden¹ and Yoram Moses^{2
  1} University of Technology, Australia
  ² Technion, Israel
  
  
• Supporting Contexts in the Sequential Real-Time Refinement Calculus
  Luke Wildman and Ian Hayes
  University of Queensland, Australia
  
  
• Inheritance in Larch Interface Specification Languages, Its Semantic Foundation and Formal Semantics
  Yoonsik Cheon
  Systems Engineering Research Institute, Republic of Korea

Session V: Friday 1200

IRW/FMP
Robertson Theatre

• The Essence of Expression Refinement
  Martin Schwenke¹ and Brendan Mahony^{2
  1}Australian National University, Australia
  ²Defence Science and Technology Organisation, Australia
  
  
• Expression Refinement in Higher Order Logic
  Brendan Mahony
  Defence Science and Technology Organisation, Australia

Session W: Friday 1430

IRW/FMP
Robertson Theatre

• Data Refining Logic Programs
  Robert Colvin, Ian Hayes, and Paul Strooper
  University of Queensland, Australia
  
  
• Grey Box Data Refinement
  Eerke Boiten and John Derrick
  University of Kent, United Kingdom

TPHOLs'98 Papers

Note that the notation "[X]" indicates the paper is presented in session X.

TPHOLs'98 Invited Papers

[J]

Verified Lexical Analysis
Tobias Nipkow
Technische Universität München, Germany

[G]

Extending Window Inference
Joakim von Wright
Åbo Akademi University, Finland

TPHOLs'98 Refereed Papers

[N1]

Program Abstraction in a Higher Order Logic Framework
Marco Benini, Sara Kalvala, and Dirk Nowotka
University of Warwick, UK

[D2]

The Village Telephone System: A Case Study in Formal Software Engineering
Karthikeyan Bhargavan,¹ Carl Gunter,¹ Elsa Gunter,² Michael Jackson,³ Davor Obradovic,¹ and Pamela Zave^3
1University of Pennsylvania, United States
²Bell Labs, United States
³AT&T Labs, United States

[E2]

Generating Embeddings from Denotational Descriptions
Richard Boulton
University of Edinburgh, United Kingdom

[R2]

An Interface between Clam and HOL
Richard Boulton,¹ Konrad Slind,² Alan Bundy,¹ and Mike Gordon^2
1University of Edinburgh, United Kingdom
²University of Cambridge, United Kingdom

[P1]

Classical Propositional Decidability via Nuprl Proof Extraction
James Caldwell
Cornell University and NASA Ames Research Center, United States

[M1]

A Comparison of PVS and Isabelle-HOL
David Griffioen,¹ and Marieke Huisman^2
1CWI, The Netherlands
²University Nijmegen, The Netherlands

[R1]

Adding External Decision Procedures to HOL90 Securely
Elsa Gunter
Bell Laboratories, United States

[Q2]

Formalizing Basic First Order Model Theory
John Harrison
Intel

[C2]

Formalizing Dijkstra
John Harrison
Intel

[E1]

Mechanical Verification of Total Correctness Through Diversion Verification Conditions
Peter Homeier and David Martin
University of Pennsylvania, United States

[M2]

A Type Annotation Scheme for Nuprl
Douglas Howe
Bell Labs, United States

[D3]

Verifying a Garbage Collection Algorithm
Paul Jackson
University of Edinburgh, United Kingdom

[P2]

HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux
Karsten Konrad
Universität des Saarlandes, Germany

[F2]

Free Variables and Subexpressions in Higher-Order Meta Logic
Chuck Liang
Trinity College, United States

[F1]

An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction
Maxim Lifantsev and Leo Bachmair
SUNY, United States

[Q1]

Proving Isomorphism of First-Order Logic Proof Systems in HOL
Anna Mikhajlova and Joakim von Wright
Åbo Akademi University, Finland

[L2]

Exploiting Parallelism In Interactive Theorem Provers
Roderick Moten
Colgate University, United States

[L1]

I-O Automata and Beyond - Temporal Logic and Abstraction in Isabelle
Olaf Müller
Technische Universität München, Germany

[D1]

Object-Oriented Verification based on Record Subtyping in Higher-Order Logic
Wolfgang Narashewski and Markus Wenzel
Technische Universität München, Germany

[N2]

On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System
Naren Narasimhan and Ranga Vemuri
University of Cincinnati, United States

[N3]

Co-Inductive Axiomatization of a Synchronous Language
David Nowak, Jean-René Beauvais, and Jean-Pierre Talpin
IRISA, France

[B1]

Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling
François Puitg and Jean-François Dufourd
LSIIT, France

[C1]

A Tool for Data Refinement
Rimvydas Ruksenas and Joakim von Wright
Åbo Akademi University, Finland

[P3]

Mechanizing Relevant Logic with HOL
Hajime Sawamura and Daisaku Asunuma
Niigata University, Japan

[F3]

Case Studies in Meta-Level Theorem Proving
Friedrich von Henke, Stephan Pfab, Holger Pfeifer, and Harald Ruess
Universität Ulm, Germany

[B2]

Formalization of Graph Search Algorithms and Its Applications
Mitsuharu Yamamoto,¹ Koichi Takahashi,² Masami Hagiya,² Shim-ya Nishizaki,¹ and Tetsuo Tamai^2
1Chiba University, Japan
²University of Tokyo, Japan

TPHOLs'98 Work in Progress Papers

[K2]

Integrating TPS with Omega
Christoph Benzmuller and Volker Sorge
Univerität des Saalandes; Germany

[A3]

Some Theorem Proving Aids
Paul E. Black¹ and Phillip J. Windley^2
1National Institute of Standards and Technology
²Brigham Young University

[A4]

Verification of the MDG Components Library in HOL
Paul Curzon,¹ Sofiène Tahar,² and Otmane Aït Mohamed^3
1Middlesex University, United Kingdom
²Concordia University, Canada
³University of Montreal, Canada

[A6]

Simulating Term-Rewriting in LPF and in Display Logic
Jeremy E. Dawson
The Australian National University, Australia

[K5]

A Prototype Generic Tool Supporting the Embedding of Formal Notations
Andrew M. Gravell and Chris H. Pratten
University of Southampton, United Kingdom

[A1]

Embedding a Formal Notation: Experiences of Automating the Embedding of Z in the Higher Order Logics of PVS and HOL
Andrew M. Gravell and Chris H. Pratten
University of Southampton, United Kingdom

[A5]

Building HOL90 Everywhere Easily (Well Almost)
Elsa L. Gunter
Bell Laboratories, United States

[K4]

Program Composition in Coq-Unity
François Marques
France Telecom, France

[K3]

Formally Analysed Dynamic Synthesis of Hardware
Kong Woei Susanto and Tom Melham
University of Glasgow, United Kingdom

[A2]

Requirements for a Simple Proof Checker
Geoffrey Watson
University of Queensland, Australia

[K1]

Integrating HOL and RAISE: A Practitioner's Approach
Wai Wong¹ and Karl R. P. H. Leung^2
1Hong Kong Baptist University, Hong Kong
²Hong Kong Polytechnic University, Hong Kong