Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Thu, 17 Sep 92 13:45:46-0100
Message-Id: <9209171345.AA10158@esat.kuleuven.ac.be>
Original-Received: by esat.kuleuven.ac.be Thu, 
                   17 Sep 92 13:45:48-0100
PP-warning: Illegal Received field on preceding line
From: claesen@be.imec
To: infohol@.m
Subject: Latex file of |- HOL'92 program.

\documentstyle[12pt]{article}
\textheight 25.5cm
\textwidth 16cm
\title{HIGHER ORDER LOGIC THEOREM PROVING AND ITS APPLICATIONS.}
\oddsidemargin 0cm
\evensidemargin 0cm
\topmargin -1.8cm
\pagestyle{empty}
\author{
International Workshop $\vdash$HOL'92  \\ 
CHEOPS ESPRIT BRA - IFIP 10.2}
\date{21-24 September 1992 - IMEC Leuven Belgium}

\begin{document}
\maketitle

This scientific meeting is the fifth in a series of annual workshops focusing  
arround the topic of higher order logic theorem proving, its usage in the HOL 
system and its applications. Previous workshops have taken place in Cambridge 
UK, Aarhus Denmark and Davis California.

The HOL system is a higher order logic theorem proving system implemented at
Cambridge University.  It has found many applications, from the verification 
of hardware designs at all levels to the verification of programs and 
communication protocols. 
Besides HOL, also contributions and experiences with other higher order logic 
based systems will be presented. 

Presentations and discussions are related to all topics concerning higher 
order logic theorem proving and its applications.  
This includes the following subjects:

\begin{itemize}
\item  Formal Hardware Design and Verification. 
\item Formal Software Design and Verification. 
\item  System Level Verification.
\item Transformational Design.
\item Hardware / Software co-Design.
\item Basic Proof Techniques and Developments.
\item Industrial applications of higher order logic proving.
\item Trade off Theorem Proving / OBDD's.
\item  Efficient implementations of higher order logic.
\item  Embedding other formalisms in higher order logic.
\item  Interfacing with hardware description languages.
\item User interface aspects of interactive proof.
\item Practical experiences.
\end{itemize}

\newpage
\section*{Monday 21 September 1992 }

Registration \& Welcome. (8.30 - 9.00)


\subsubsection*{New extensions to the HOL system. (1) (9.00 - 10.30)} 
{\em session chair: Mike Gordon}
\begin{itemize}
\item "The HOL Logic Extended with Quantification over Type Variables", T.F. Melham,
University of Cambridge, UK.

\item "Abstract Theories in HOL", Phillip J. Windley, University of Idaho, USA.

\item "New Concepts in Faust", Klaus Schneider, Ramaya Kumar, Thomas Kropf,
University of Karlsruhe, Germany
\end{itemize}

coffee break (10.30 - 11.00)

\subsubsection*{Induction (11.00 - 12.30)} 
{\em session chair: Elsa Gunter}
\begin{itemize}
\item 
"Unification-Based Induction", Holger Bush, Siemens AG Munchen, Germany.
\item 
"Introducing well-founded function definitions in HOL", Mark van der Voort,
University of Twente, The Netherlands.
\item 
"Boyer-Moore Automation for the HOL System", Richard J. Boulton, 
University of Cambridge, UK.
\end{itemize}
 
lunch (12.30 - 14.00)

\subsubsection*{Programming languages: refinements and proofs. (14.00 - 15.30)} 
{\em session chair: Andrew Gordon}
\begin{itemize}
\item
"A Mechanisation of some Advanced Refinement Concepts", Joakim von Wright,
J. Hekanaho, P. Luostarinen and T. Langbacka,
Abo Akademi University, Turku, Finland.
\item 
"Deriving Correctness Properties of Compiled Code", Paul Curzon,
University of Cambridge, UK.
\item 
"A HOL Mechanization of The Axiomatic Semantics of a Simple Distributed
Programming Language", William L. Harrison, University of Illinois,
Karl N. Levitt, Myla Archer, University of California Davis, USA.
\end{itemize}

coffee break (15.30 - 16.00)

\subsubsection*{Microprocessor verification methodologies. (16.00 - 17.30)} 
{\em session chair: Myla Archer}
\begin{itemize} \item
"A Methodology for Reusable Hardware Proofs", Mark Aagaard, Miriam Leeser,
Cornell University, Ithaca, USA.
\item 
"Towards a Formal Verification of a Floating Point Coprocessor and its
Composition with a Central Processing Unit", Jing Pan, Karl Levitt,
Myla Archer, Sara  Kalvala, University of California, Davis, USA.
\item 
"Machine Abstraction in Microprocessor Specification", Michael McAllister,
University of British Columbia, Canada.
\end{itemize}

(17.30 - 20.00) Dinner

(starting 20.00) Old Flemish Games \& Belgian beer tasting evening.

\section*{Tuesday 22 September 1992 }

\subsubsection*{Tutorial: (9.00 - 10.00)}
\begin{itemize} \item 
"ProofPower", Roger B. Jones, ICL UK.
\end{itemize}

coffee break (10.00 - 10.30)

\subsubsection*{Proof of Automata. (10.30 - 12.30)}
{\em session chair: Phillip J. Windley}
\begin{itemize}
\item 
"A Comparison between Statecharts and State Transition Assertions", Nancy Day,
University of British Columbia, Canada.
\item 
"Formalizing a Modal Logic for CSS in the HOL Theorem Prover", Monica Nesi,
University of Cambridge, UK.
\item 
"An Embedding of Timed Transition Systems in HOL", Rachel Cardell-Oliver, 
Roger Hale, John Herbert, Cambridge Computer Science Research Centre, SRI
International, UK.
\item 
"A Principle of Definition for Primitive Rules of Inference in hol90", Konrad
Slind, Bell Labs, USA.
\item 
"A Formal Theory of Infinite Automata", Paul Loewenstein, Sun Microsystems,
Palo Alto, USA.
\end{itemize}

lunch (12.30 - 14.00)

social event - outing (14.00 - 18.00)


\subsubsection*{Hardware Description Languages and Proof Methodologies. (18.00 - 19.30)}
{\em session chair: Tim Leonard}

   
\begin{itemize} \item 
"A Formalisation of the VHDL Simulation Cycle", John P. Van Tassel, University
of Cambridge, UK.
\item
"The Formal Semantics Definition of a Multi-rate DSP language in HOL", C.M.
Angelo, L. Claesen, H. De Man, IMEC Leuven, Belgium.
\item 
"Implementation and Use of Annotations in HOL", Sara Kalvala, Myla Archer, Karl
Levitt, University of California, Davis, USA.
\end{itemize}
 
conference dinner (start at 20.00).

\section*{Wednesday 23 September 1992}

\subsubsection*{Tutorial: (9.00 - 10.00)}\
{\em session chair: John Herbert}

\begin{itemize} \item 
"Hybrid Formal Hardware Verification Techniques", Jeff Joyce, Carl Seger,
University of British Columbia, Canada.
\end{itemize}

coffee break (10.00 - 10.30)

\subsubsection*{Efficient Proof Methods, Hardware Simulation and Reasoning (10.30 - 12.30)}
{\em session chair: Ramayya Kumar}

\begin{itemize} \item 
"A Lazy Approach to Fully-Expansive Theorem Proving", Richard Boulton,
University of Cambridge, UK.
\item 
"Operational Semantics Based Formal Symbolic Simulation", K. Goossens,
University of Edinburgh, UK
\item 
"Formal Tools for Tri-State Design in Busses", R.B. Hughes, M.D. Francis,
S.P. Finn, G. Musgrave, Abstract Hardware Ltd. \& Brunel University, UK.
\item 
"Simulating Microprocessors from Formal Specifications", Kelly M. Hall,
Phillip J. Windley, University of Idaho, USA.
\end{itemize}

lunch (12.30 - 14.00)

\subsubsection*{Parallel Session 1: New Extensions to the HOL system (2) (14.00 - 17.30)}
{\em session chair: Tom Melham}
\begin{itemize} 
\item 
"Linking Other Theorem Provers to HOL Using PM: Proof Manager", Myla Archer,
George Fink, Lie Yang, University of California, Davis, USA.
\item 
"Why we can't have SML Style datatype Declarations in HOL", Elsa L. Gunter,
AT\&T Bell Labs, USA.
\item
"What's going on in hol90?", Konrad Slind, University of Calgary, Canada.
\item "Changes in HOL-88 version 2.01", John Harrison, Cambridge University,
UK.  
\item 
"Executing HOL Specifications: Towards an Evaluation Semantics for 
Classical Higher Order Logic", Sreeranga Rajan, University of British 
Columbia, Canada.
\end{itemize}

coffee break (15.30 - 16.00)


\subsubsection*{HOL clinic, late news \& HOL convention (16.00 - 17.30) }

{\em session chair: Tom Melham}


\subsubsection*{Parallel Session 2: LAMBDA-specifics and users meeting. (14.00-17.30)} 
{\em session chair: Holger Busch}

(seminar room 1.D IMEC)

\begin{itemize} \item 
"Deriving a Correct Computer", Li-Guo Wang, University of Edinburgh, UK.
\item 
"Design-Flow Graph Partioning", R.B. Hughes, G. Musgrave, Abstract Hardware
Ltd., Brunel University, UK>
\item 
"Specification and Formal Synthesis of Digital Circuits", M. Bombana, P.
Cavalloro, G. Zaza, ITALTEL - DRSC Milan, Italy.
\item LAMBDA users meeting (chair Holger Busch).
\end{itemize}


coffee break (15.30 - 16.00)

dinner (18.00 - 20.00)

volleyball (starts arround 20.00)

\section*{Thursday 24 September 1992 (9.00 - 13.00)}

\subsubsection*{Proof Methodologies and Theories. (1) (9.00 - 10.30)} 

{\em session chair: Carl Seger}

\begin{itemize} \item 
"Constructing the real numbers in HOL", John Harrison, University of
Cambridge, UK.
\item 
"Modelling Generic Hardware Structures by Abstract Datatypes", Klaus Schneider,
Ramayya Kumar, Thomas Kropf, University of Karlsruhe, Germany.
\item 
"Modeling Non-Deterministic Systems in HOL", Jim Alves-Foss, University of
Idaho, USA.
\end{itemize}
 
coffee break (10.30 - 11.00)

\subsubsection*{Proof Methodologies and Theories. (2) (11.00 - 12.30)}

{\em session chair: Jeff Joyce}

\begin{itemize} 
\item 
"A Sequent Formulation of the Propositional Logic of Predicates in HOL",
Ching-Tsun Chou, University of California, Los Angeles, USA.
\item 
"A Note on Interactive Theorem Proving with Theorem Continuation Functions",
Ching-Tsun Chou, University of California, Los Angeles, USA.
\item 
"A Classical Type Theory with Transinite Types", Garrel Pottinger,
ORA \& Cornell University, USA.
\end{itemize}

closing of the workshop.

(12.30 - 14.00) lunch

\vspace*{2cm}

BUS TRANSPORTATION FROM THE HOTELS IN THE MORNING AND TO THE HOTELS IN THE
EVENING IS FORESEEN.

\end{document}