Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 20 May 1994 16:38:27 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA06094; Fri, 20 May 1994 09:15:27 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA06090; Fri, 20 May 1994 09:15:20 -0600 Received: from vanuata.dcs.gla.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA04169; Fri, 20 May 1994 08:15:06 -0700 Received: from hawaii.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk with LOCAL SMTP (PP) id <13826-0@goggins.dcs.gla.ac.uk>; Fri, 20 May 1994 16:04:39 +0100 Received: by hawaii.dcs.gla.ac.uk (4.1/Dumb) id AA08552; Fri, 20 May 94 16:04:28 BST From: hug94 Message-Id: <9405201504.AA08552@hawaii.dcs.gla.ac.uk> To: info-hol@cs.uidaho.edu Cc: hug94@dcs.gla.ac.uk Subject: HUG94 - Preliminary Programme Information. Date: Fri, 20 May 94 16:04:27 +0100 Full programme and registration information for this year's conference on higher order logic theorem proving and its applications will be announced very soon. Meanwhile, please see the attached preliminary announcement of the scientific programme. As you can see, we have a very interesting and varied conference in store for us! Tom Melham Programme Chair HUG-94 ********************************************************************* 7th International Workshop on Higher Order Logic Theorem Proving and its Applications Malta, 19-22 September 1994 ********************************************************************* ********************** Provisional Programme ************************ ********************************************************************* ===================================================================== The following papers will be presented under Category A: --------------------------------------------------------------------- First-order automation for HOL-proofs Holger Busch Simplifying Deep Embedding: A Formalised Code Generator Ralf Reetz and Thomas Kropf Automating Verification by Functional Abstraction at the System Level Klaus Schneider, Ramayya Kumar, and Thomas Kropf Representing higher-order logic proofs in HOL J. von Wright Providing Tractable Security Analyses in HOL Stephen H. Brackin Mechanical verification of Distributed Algorithms in Higher-Order Logic Ching-Tsun Chou A Formal Theory of Undirected Graphs in Higher-Order Logic Ching-Tsun Chou Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator Peter V. Homeier and David F. Martin Towards a Mechanically Supported and Compositional Calculus to Design Distributed Algorithms ISWB Prasetya A Graphical Tool for Proving Progress Flemming Andersen, Kim Dam Petersen, and Jimmi S. Pettersson Symbolic Animation as a Proof Tool Juanito Camilleri and Vincent Zammit An Engineering Approach to Formal Digital System Design Mats Larsson A HOL Formalisation of the Temporal Logic of Actions Thomas L{\aa}ngbacka Studying the ML Module System in HOL Savi Maharaj and Elsa Gunter LCF Examples in HOL Sten Agerholm Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics Juin-Yeu Lu and Shiu-Kai Chin An Interpretation of NODEN in HOL Brian Graham Tracking Design Changes with Formal Verification: A Network Component Case Study Paul Curzon Datatypes in L2 Nick Chapman, Simon Finn, and Michael P. Fourman Towards a HOL theory of memory J-P. Bodeveix, M. Filali, and P. Roche Reasoning about Linear Systems of Equations in HOL Catia M. Angelo, Luc Claesen, and Hugo De Man S: A Machine Readable Specification Notation based on Higher Order Logic J. Joyce, N. Day, and M. Donat Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL Sofi\`{e}ne Tahar and Ramayya Kumar Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circuit Behavior David A. Fura and Arun K. Somani A Parameterized Proof Manager Konrad Slind Architectural Specification in HOL Phillip J. Windley Binary Decision Diagrams as a HOL Derived Rule John Harrison ==================================================================== The following papers will be presented under Category B: -------------------------------------------------------------------- Why Hardware Verification Needs more than Model Checking Klaus Schneider, Ramayya Kumar, Thomas Kropf A Higher-order Theory of Lists for HOL Paul Curzon, Wai Wong Trustworthy Tools for Trustworthy Programs: Automatic Verification of Mutually Recursive Procedures Peter Homeier and David Martin Evaluation Techniques as a Part of the Verification Process Dirk Eisenbiegler and Ramayya Kumar Towards Efficient Conversions by use of Partial Evaluation Morten Welinder Towards a Formal Verification of a Secure and Distributed System and Applications Zhang, Shaw, Heckman, Benson, Beard, Archer, Levitt, Olsson A Tree-Based, Graphical Interface for Large Proof Development Tom Schubert and John Biggs Formal Reasoning about Specification and Transformation of Reactive Systems Jurgen Bohn A Interpreter Interface Language and Its Formal Embedding in Higher-Order Logic David Fura and Arun Somani A Reference Version of HOL John Harrison and Konrad Slind Using Make to Manage Large Proofs Philip J. Windley Not Implementing N-Bit Words by Using Abstract Theories Philip J. Windley ===================================================================== 7th International Workshop on Higher Order Logic Theorem Proving and its Applications Malta, 19-22 September 1994. PROGRAMME CHAIR WORKSHOP CHAIR =============== ============== Dr. Thomas Melham Dr. Juanito Camilleri Dept. of Computer Science Dept. of Computer Science & AI University of Glasgow University of Malta 17 Lilybank Gardens University Heights Glasgow, Scotland, G12 8QQ Tal-Qroqq, Malta e-mail: tfm@dcs.glasgow.ac.uk e-mail: jac1@cl.cam.ac.uk For further information, contact the programme chair by post at the address given above or by email, preferably at hug94@dcs.glasgow.ac.uk. =====================================================================