Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 16 Jun 1993 08:45:42 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13239; Tue, 15 Jun 93 21:48:32 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA13234; Tue, 15 Jun 93 21:48:24 -0700 Received: by grolsch.cs.ubc.ca id AA15679 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Tue, 15 Jun 1993 21:48:45 -0700 Date: 15 Jun 93 21:48 -0700 From: hug93 To: info-hol Message-Id: <127*hug93@cs.ubc.ca> Subject: HUG'93 preliminary program Preliminary Program and Second Call for Participation 1993 International Meeting on H I G H E R O R D E R L O G I C T H E O R E M P R O V I N G A N D I T S A P P L I C A T I O N S Tutorials and Workshops August 10-13 1993 The University of British Columbia Vancouver - Canada *********************************************************************** * * * HUG'93 Workshop - August 11-13 * * * *********************************************************************** The following is a preliminary, tentative program for the 3-day workshop: Wednesday, August 11, 1993 ========================== 08:00-08:20 Registration 08:20-08:30 Welcome, HUG'93 chair Session 1: Embedded Formalisms/Theories I ========== 08:30-08:50 "Program Verification using HOL-UNITY", F. Andersen, K. D. Petersen, and J. S. Petterson, Tele Danmark Research 08:50-09:10 "Graph model of LAMBDA in Higher Order Logic", K. D. Petersen, TFL, Danmark 09:10-09:30 "Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL", C. Zhang, R. Shaw, R. Olsson, K. Levitt, M. Archer, M. Heckman, and G. Benson, U. of California, Davis, USA 09:30-09:50 "Reasoning with the Formal Definition of Standard ML in HOL", D. Syme, Australian National University, Australia 09:50-10:10 "HOL-ML", M. VanInwegen and E. Gunter, U. of Pennsylvania, USA 10:10-10:30 Coffee break Session 2: Keynote Address I =========== 10:30-11:30 Paul Gilmore, Professor Emeritus, Department of Computer Science, U. of British Columbia, Canada 11:30-13:00 Lunch Session 3: Applications I ========== 13:00-13:20 "Structure and Behaviour in Hardware Verification", K. Goossens, U. of Edinburgh, UK 13:20-13:40 "Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL", C. M. Angelo, L. Claesen, and I. Man, IMEC, Belgium 13:40-14:00 "Linking HOL to a VLSI CAD System", S. Chin and J. Lu, Syracuse University, USA 14:00-14:20 "A Functional Approach for Formalizing Regular Hardware Structures", D. Eisenbiegler, K. Schneider, R. Kumar, Forschungszenntrum Informatik, Germany 14:20-14:40 Coffee break Session 4: Theory/System Infrastructure I ========== 14:40-15:00 "A Proof Development System for HOL", L. Thery, U. of Cambridge, UK and INRIA, France 15:00-15:20 "Reasoning with Inductively Defined Mutually Recursive Relations in the HOL Theorem Prover", R. Roxas, Australian National University, Australia 15:20-15:40 "A Broader Class of Trees for Recursive Type Definitions for HOL", E. Gunter, AT&T Laboratories, USA 15:40-16:00 Break 16:00-16:20 "Theorems We Should Prove", D. Parnas, McMaster University, Canada Session 5: System Demonstration I ========== 16:20-17:00 PVS Introduction and Demonstration, SRI International Thursday, August 12, 1993 ========================== Session 6: Keynote Address II ========== 08:30-09:30 D. Parnas, Professor Department of Electrical and Computer Engineering, McMaster University, Canada 09:30-10:00 Coffee break Session 7: Hybrid Systems ========== 10:00-10:20 "Extending the HOL theorem prover with a Computer Algebra System to Reason about the Reals", J. Harrison and L. Thery, U. of Cambridge, UK 10:20-10:40 "The HOL-Voss System: Interactive Theorem-Proving combined with Trajectory Evaluation", J. Joyce and C. Seger, U. of British Columbia, Canada 10:40-11:00 "The Semantics of Statecharts in HOL", N. Day, and J. Joyce, U. of British Columbia, Canada 11:00-11:20 "Alternative Proof Procedures for Finite-State Machines in a Higher Order Environment", K. Schneider, R. Kumar, and T. Kropf, U. of Karlsruhe, Germany 11:20-11:40 "A Formalization of Abstraction in LAMBDA", A. McIsaac, U. of Edinburgh, UK 11:40-13:00 Lunch Session 8: Applications II ========== 13:00-13:20 "Report on the UCD Microcoded Viper Verification Project", T. Schubert, U. of California, USA 13:20-13:40 "Verification of Tamarack-3 Microprocessor in a Hybrid Verification Environment", Z. Zhu, J. Joyce, and C. Seger U. of British Columbia, Canada 13:40-14:00 "Abstraction Techniques for Modeling Real-World Interface Chips", D. A. Fura, P.J. Windley, and A.K. Somani, The Boeing Company, Seattle, USA 14:00-14:20 "Implementing a Methodology for Formally Verifying RISC Processors in HOL", R. Kumar and S. Tahar, U. of Karlsruhe, Germany 14:20-14:40 Coffee break Session 9: Embedded Formalisms/Theories II ========== 14:40-15:00 "Domain Theory in HOL", S. Agerholm, Aarhus University, Danmark 15:00-15:20 "Predicates, Temporal Logic, and Simulations", C-T. Chou, U. of California, USA 15:20-15:40 "Formalization of Variables Access Constrains to Support Compositionality of Liveness Properties", W. Prasetya, Vakgroep Informatica, Nederland 15:40-16:00 "Value-Passing CCS in HOL", M. Nesi, U. of Cambridge, UK Session 10: System Demonstrations II =========== 16:00-16:40 TPS Introduction and Demonstration, P. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning and H. Xi, Carnegie Mellon University, USA Friday, August 13, 1993 ======================= Session 11: Applications III =========== 08:30-08:50 "Modelling Bit Vectors in HOL: the `word' Library", W. Wong, U. of Cambridge, UK 08:50-09:10 "Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification", K. Schneider, R. Kumar, and T. Kropf, U. of Karlsruhe, Germany 09:10-09:30 "Toward a Super Duper Hardware Tactic", M. Aagaard, M. Leeser, P. Windley, Cornell University, USA 09:30-09:50 Coffee break Session 12: Theory/System Infrastructure II =========== 09:50-10:10 "A mechanisation of name-carrying syntax up to alpha-conversion", A. Gordon, Chalmers University of Tech. and U. of Goteborg, Sweden 10:10-10:30 "A HOL Decision Procedure for Elementary Real Algebra", J. Harrison, U. of Cambridge, UK 10:30-10:50 "AC Unification in hol90", K. Slind, Germany Session 13: System Demonstrations III =========== 10:50-11:30 Nuplr Introduction and Demonstration, M. Aagaard and M. Leeser, Cornell University 11:30-13:00 Lunch Session 14: Applications III =========== 13:00-13:20 "Server-Process Restrictiveness in HOL", S-K. Chin and S. H. Brackin, Syracuse University, USA 13:20-13:40 "Safety in Railway Signalling Data: A Behavioural Analysis", M.J. Morley, U. of Edinburgh, UK 13:40-14:00 "On the Style of Mechanical Proving", I. Prasetya, Vakgroep Informatica, Nederland 14:00-14:20 "From Abstract Data Types to Shift Registers", S. Rajan, J. Joyce, C. Seger, U. of British Columbia, Canada 14:20-14:40 "Verification in Higher Order Logic of Mutual Exclusion Algorithm", V. Carreno, NASA Langley RC, USA 14:40-15:00 Coffee break Sessions 15: Group Discussions ============ 15:00-16:00 Focused group discussions 16:00-16:30 Reports from discussions 16:30-16:45 HUG'94 Preparation Meeting 16:45-17:00 Conclusions/Wrap-up *********************************************************************** * * * HUG'93 Tutorials - August 10 * * * *********************************************************************** Two parallel 1-day tutorials will be offered on Tuesday, August 10: (a) Introduction to the HOL System and Its Applications. ---------------------------------------------------- This tutorial will provide an introduction to the notation of higher-order logic and its principles of definition and formal reasoning. Part of the tutorial will describe how the notation of higher-order logic can be used as a specification language for a variety of application domains. The tutorial will also explain how other formalisms and specification languages can be embedded semantically inside higher-order logic allowing the HOL System to be used as a software tool for developing rigorous interfaces between a variety of formalisms and/or specification languages. The tutorial will include some hands-on laboratory exercises. This 1-day tutorial is intended mainly for HUG'93 participants who might not necessarily be familiar with the HOL System and would benefit from an overview of the system in preparation for participation in the workshop. (b) Introduction to the NaDSet and its Applications. ------------------------------------------------ NaDSet is a natural deduction-based set theory and logic that formalizes logical connectives, quantifiers and set abstraction through rules of deduction rather than axioms. NaDSet is particularly useful for the definition of inductively defined sets. Induction rules can be derived from these inductive definitions rather than being introduced as primitive rules of reasoning. In particular NaDSet provides a logical foundation for structured operational semantics, for category theory and for non-well-founded sets. In addition to a discussion of NaDSet, the tutorial will describe experience in building and using a theorem-prover implemented in a commercial-based Meta-CASE tool, the REFINE System from Reasoning Systems, Inc. This 1-day tutorial is offered to HUG'93 participants as an alternative to the above "Introduction to the HOL System and Its Application" tutorial. *********************************************************************** * * * HUG'93 Organization * * * *********************************************************************** Organization: ============= Jeffrey Joyce (Co-Chair & Finance) Carl-Johan Seger (Co-Chair & Program) Zheng Zhu (Publicity) Jane Hutton (Administration) Vicki Ayerbe Eric Borm Nancy Day Mike Donat Paul Gilmore Andrew Martin Sree Rajan Program Committee: ================= Carl-Johan Seger University of British Columbia, Canada (Chair) Jim Alves-Foss University of Idaho, USA Luc Claesen IMEC & Kath. Univ. Leuven, Belgium John Herbert SRI International, UK Jeffrey Joyce University of British Columbia, Canada Tom Melham Computer Laboratory, University of Cambridge, UK David Shepherd INMOS Ltd., UK Phillip Windley Brigham Young University, USA *********************************************************************** * * * Other HUG'93 Activities * * * *********************************************************************** + Sailing Excursion, Monday, August 9, 14:00-17:00 (reservations should be made by June 18, more information is available by anonymous ftp from cs.ubc.ca at /pub/local/hug93/Sailing.txt) + Informal Reception, Wednesday, August 11, 18:00-19:30 + Conference Banquet, Thursday, August 12, 18:30-22:30 + outdoor sports activities (e.g., volleyball, ultimate) are likely to be organized during the evenings of August 9, 10, 11 and 13. + it is possible that we may informally organize another excursion (as an alternative to the Sailing Excursion) on Monday, August 9, (e.g., a walk in the local mountains). + we expect to informally organize "restaurant excursions" on the evenings of August 9, 10, 11 and 13 where some of the organizers and other locals will lead small groups to favorite Vancouver restaurants for dinner. *********************************************************************** * * * Other Events * * * *********************************************************************** Formal Hardware Verification Course -- August 4-6 =================================================== An intensive 3-day course on formal hardware verification will be held August 4-6 at UBC. The course instructors, J. Joyce and C-J. Seger, will describe methods such as symbolic simulation, trajectory evaluation and model checking which complement the strengths of theorem-proving based approaches. This course will also describe how theorem-proving methods can be combined with these other formal approaches to obtain hybrid approaches to formal hardware verification. This course will include hands-on laboratory exercises. A description of this course and registration information is available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see FHV.{txt|ps}. Although the course is organized separately from HUG'93, it has been scheduled in conjunction with HUG'93 for the convenience of those who may wish to participate in both events. *********************************************************************** * * * Registration Information * * * *********************************************************************** By June 21st After June 21st Students Half-day ------------ --------------- -------- -------- HOL/NaDSet Tutorial $35 $50 $25 HUG'93 $275 $350 $150 $50 The half-day rate of $50 ($25 for students) includes admission to either a morning or afternoon session. It does not include a copy of the proceedings (which can be purchased separately) or the workshop banquet. Prospective participants should use a copy of the registration form to register in a tutorial and/or the workshop. These forms are available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see HUG93Reg.{txt|ps}. *********************************************************************** * * * Accommodation Information * * * *********************************************************************** A limited number of rooms (private bedroom, shared bathroom) have been reserved for course participants at $32 per night plus taxes. Other accommodation may also be available at a reduced rate. This accommodation should be booked by July 20. Prospective participants should use a copy of the "request for accommodation" form to make accommodation arrangements. This form is available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see Accommodation.{txt|ps}. It is possible that our block of reserved accommodation will be fully booked by HUG'93 participants before July 20. To avoid disappointment, book your accommodation early ! *********************************************************************** * * * Obtaining HUG'93 Information Via ftp * * * *********************************************************************** This and previous announcements of HUG'93 are available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93. "*" in the file extension indicates that the file has two different versions: ascii (.txt) and Postscript (.ps.Z): Filenames Contents ---------------- ------------------------------------------------- Accommodation.* Accommodation information and the request form Announce1.* The first announcement and call-for-participation for HUG'93 Announce2.* The second announcement and call-for-participation for HUG'93 CFPaper1.* Call-for-paper of HUG'93 FHV.* Description and registration form of the formal hardware verification course HUG93Reg.* Registration form HUG'93 and HOL/NaDSet tutorials parnas.ps.Z David Parnas's article on "What Theorems Should We Prove" dac93.ps.Z A description of HOL-Voss system Sailing.txt Registration form for sailing excursion during HUG93 Program.* The HUG'93 program (to be regularly updated). llncs.tar.Z Springer-Verlag's LaTeX format files. It contains .sty files, an example and a brief introduction. If you experience any difficulty in accessing the ftp directory, you are encouraged to contact us at: Email: hug93@cs.ubc.ca (Preferred) FAX: (604)-822-5485 Phone: (604)-822-6176