Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Fri, 21 Aug 1992 21:54:16 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23535; Fri, 21 Aug 92 12:47:08 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from n-kulcs.cs.kuleuven.ac.be by ted.cs.uidaho.edu (16.6/1.34) id AA23530; Fri, 21 Aug 92 12:46:42 -0700 Received: from gpx3u.esat.kuleuven.ac.be by n-kulcs.cs.kuleuven.ac.be (5.65b/n_kulcs1.1) id AA08864; Fri, 21 Aug 92 21:43:04 +0200 Date: Fri, 21 Aug 92 20:46:16-0100 Message-Id: <9208212046.AA04119@esat.kuleuven.ac.be> Original-Received: by esat.kuleuven.ac.be Fri, 21 Aug 92 20:46:17-0100 PP-warning: Illegal Received field on preceding line From: claesen@be.imec To: infohol@.m Subject: |- HOL92 program ============================================================================== Call for Participation 21-24 September 1992 1992 International Workshop on | H H OOOOO L '' 99999 22222 | H H O O L ' 9 9 2 2 | H H O O L ' 9 9 2 |------ HHHHHHHH O O L 999999 2 | H H O O L 9 2 | H H O O L 9 9 2 | H H OOOOO LLLLLLL 99999 2222222 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. in cooperation with: ESPRIT CHEOPS BRA, IFIP 10.2 IMEC - Leuven - Belgium ============================================================================== 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. TOPICS. ======= Presentations and discussions are related to all topics concerning higher order logic theorem proving and its applications in HOL and/or other higher order logic based theorem provers. This includes the following subjects: * Formal Hardware Design and Verification. * Formal Software Design and Verification. * System Level Verification. * Transformational Design. * Hardware / Software co-Design. * Basic Proof Techniques and Developments. * Industrial applications of higher order logic proving. * Trade off Theorem Proving / OBDD's. * Efficient implementations of higher order logic. * Embedding other formalisms in higher order logic. * Interfacing with hardware description languages. * User interface aspects of interactive proof. * Practical experiences. PROGRAM: ======== Monday 21 September 1992 (9.00 - 17.30) ------------------------ (8.30 - 9.00) Registration & Welcome. New extensions to the HOL system. (1) (9.00 - 10.30) --------------------------------- session chair: Mike Gordon "The HOL Logic Extended with Quantification over Type Variables", T.F. Melham, University of Cambridge, UK. "Abstract Theories in HOL", Phillip J. Windley, University of Idaho, USA. "New Concepts in Faust", Klaus Schneider, Ramaya Kumar, Thomas Kropf, University of Karlsruhe, Germany coffee break (10.30 - 11.00) Induction (11.00 - 12.30) --------- session chair: Elsa Gunter "Unification-Based Induction", Holger Bush, Siemens AG Munchen, Germany. "Introducing well-founded function definitions in HOL", Mark van der Voort, University of Twente, The Netherlands. "Boyer-Moore Automation for the HOL System", Richard J. Boulton, University of Cambridge, UK. lunch (12.30 - 14.00) Programming languages: refinements and proofs. (14.00 - 15.30) ---------------------------------------------- session chair: David Shepherd "A Mechanisation of some Advanced Refinement Concepts", Joakim von Wright, J. Hekanaho, P. Luostarinen and T. Langbacka, Abo Akademi University, Turku, Finland. "Deriving Correctness Properties of Compiled Code", Paul Curzon, University of Cambridge, UK. "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. coffee break (15.30 - 16.00) Microprocessor verification methodologies. (16.00 - 17.30) ------------------------------------------ session chair: Myla Archer "A Methodology for Reusable Hardware Proofs", Mark Aagaard, Miriam Leeser, Cornell University, Ithaca, USA. "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. "Machine Abstraction in Microprocessor Specification", Michael McAllister, University of British Columbia, Canada. Tuesday 22 September 1992 ------------------------- Tutorial: (9.00 - 10.00) --------- session chair: Paul Loewenstein "ProofPower", Roger B. Jones, ICL UK. coffee break (10.00 - 10.30) Proof of Automata. (10.30 - 12.30) ------------------ session chair: Phillip J. Windley "A Formal Theory of Infinite Automata", Paul Loewenstein, Sun Microsystems, Palo Alto, USA. "A Comparison between Statecharts and State Transition Assertions", Nancy Day, University of British Columbia, Canada. "Formalizing a Modal Logic for CSS in the HOL Theorem Prover", Monica Nesi, University of Cambridge, UK. "An Embedding of Timed Transition Systems in HOL", Rachel Cardell-Oliver, Roger Hale, John Herbert, Cambridge Computer Science Research Centre, SRI International, UK. lunch (12.30 - 14.00) Hardware Description Languages and Proof Methodologies. (14.00 - 15.30) ------------------------------------------------------- session chair: Tim Leonard "A Formalisation of the VHDL Simulation Cycle", John P. Van Tassel, University of Cambridge, UK. "The Formal Semantics Definition of a Multi-rate DSP language in HOL", C.M. Angelo, L. Claesen, H. De Man, IMEC Leuven, Belgium. "Implementation and Use of Annotations in HOL", Sara Kalvala, Myla Archer, Karl Levitt, University of California, Davis, USA. coffee break (15.30 - 16.00) social event & conference dinner. Wednesday 23 September 1992 (9.00 - 17.30) --------------------------- Tutorial: (9.00 - 10.00) --------- session chair: John Herbert "Hybrid Formal Hardware Verification Techniques", Jeff Joyce, Carl Seger, University of British Columbia, Canada. coffee break (10.00 - 10.30) Efficient Proof Methods, Hardware Simulation and Reasoning (10.30 - 12.30) ---------------------------------------------------------- session chair: Ramayya Kumar "A Lazy Approach to Fully-Expansive Theorem Proving", Ricard Boulton, University of Cambridge, UK. "Operational Semantics Based Formal Symbolic Simulation", K. Goossens, University of Edinburgh, UK "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. "Simulating Microprocessors from Formal Specifications", Kelly M. Hall, Phillip J. Windley, University of Idaho, USA. lunch (12.30 - 14.00) Parallel Session 1: New Extensions to the HOL system (2) (14.00 - 17.30) ======================================================== session chair: Tom Melham "A Principle of Definition for Primitive Rules of Inference in hol90", Konrad Slind, Bell Labs, USA. "Linking Other Theorem Provers to HOL Using PM: Proof Manager", Myla Archer, George Fink, Lie Yang, University of California, Davis, USA. "Why we can't have SML Style datatype Declarations in HOL", Elsa L. Gunter, AT&T Bell Labs, USA. "Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic", Sreeranga Rajan, University of British Columbia, Canada. coffee break (15.30 - 16.00) Late news presentations. ------------------------ HOL clinic (chair: Tom Melham). ---------- Informal discussions on practical usage and implementation details for HOL. Please forward your questions and input for discussion to the session chair (email: tfm@cl.cam.ac.uk) before the workshop. HOL convention (chair : Tom Melham). (17.00 - 17.30) ------------------------------------ Discussion of practical and organizational issues and future workshops. Parallel Session 2: LAMBDA-specifics and users meeting. (14.00-17.30) ======================================================= session chair: Holger Busch "Deriving a Correct Computer", Li-Guo Wang, University of Edinburgh, UK. "Design-Flow Graph Partioning", R.B. Hughes, G. Musgrave, Abstract Hardware Ltd., Brunel University, UK> "Specification and Formal Synthesis of Digital Circuits", M. Bombana, P. Cavalloro, G. Zaza, ITALTEL - DRSC Milan, Italy. LAMBDA users meeting. --------------------- Please contact Holger Busch (email: holger@koetsier.zfe.siemens.de) for more information and proposed contributions. coffee break (15.30 - 16.00) Thursday 24 September 1992 (9.00 - 13.00) -------------------------- Proof Methodologies and Theories. (1) (9.00 - 10.30) --------------------------------- "Constructing the real numbers in HOL", John Harrison, University of Cambridge, UK. "Modelling Generic Hardware Structures by Abstract Datatypes", Klaus Schneider, Ramayya Kumar, Thomas Kropf, University of Karlsruhe, Germany. "Modeling Non-Deterministic Systems in HOL", Jim Alves-Foss, University of Idaho, USA. coffee break (10.30 - 11.00) Proof Methodologies and Theories. (2) (11.00 - 12.30) --------------------------------- "A Note on Interactive Theorem Proving with Theorem Continuation Functions", Ching-Tsun Chou, University of California, Los Angeles, USA. "A Sequent Formulation of the Propositional Logic of Predicates in HOL", Ching-Tsun Chou, University of California, Los Angeles, USA. "A Classical Type Theory with Transinite Types", Garrel Pottinger, ORA & Cornell University, USA. (12.30 - 14.00) lunch LATE NEWS SESSIONS: =================== Besides the regular program sessions with recent developments and informal discussion on the usage of HOL will be included. Participants interested in contributing should send the title and short description of their contribution to the workshop chairman. DEMONSTRATIONS and WORKSTATIONS: ================================ During the workshop SUN workstations will be available for demonstrations. Discussions on practical problems etc... Please give inform the chairman if you intend to give a demonstration. (Notice that no Internet connection via FTP will be possible). WORKSHOP CHAIR: WORKSHOP CO-CHAIR: =============== ================== Luc Claesen Michael Gordon IMEC / K.U.Leuven University of Cambridge Kapeldreef 75 Computer Laboratory B-3001 Leuven Pembroke Street Belgium Cambridge CB2 3QG phone: +32-16-281203 U.K. fax: +32-16-281515 email: mjcg@cl.cam.ac.uk email: claesen@imec.be PROGRAM COMMITTEE: ================== * Myla Archer (University of California, Davis, USA) * Graham Birtwistle (University of Calgary, CA) * Holger Bush (Siemens AG, D) * Albert Camilleri (Hewlett-Packard, UK) * Shui-Kai Chin (Syracuse University, USA) * Luc Claesen (IMEC / Kath. Univ. Leuven, B) * Simon Finn (Abstract Hardware Ltd., UK) * Michael Gordon (University of Cambridge, UK) * Elsa L. Gunter (AT\&T Bell Labs, USA) * John Herbert (SRI International, UK) * Roger B. Jones (ICL, UK) * Jeff Joyce (University of British Columbia, CA) * Ton Kalker (Philips, NL) * Matt Kaufmann (Computational Logic Inc., USA) * Kurt Keutzer (Synopsys, USA) * Ramayya Kumar (Univ. of Karlsruhe, D) * Miriam Leeser (Cornell University, USA) * Tim Leonard (Digital Equipement Corp., USA) * Paul Loewenstein (Sun Microsystems, USA) * Tom Melham (University of Cambridge, UK) * Carl Seger (University of British Columbia, CA) * David Shepherd (Inmos Ltd., UK) * Gerd Venzl (Siemens AG, D) * Phillip J. Windley (University of Idaho, USA) LOCAL ARRANGEMENTS ================== Annemie Stas IMEC - Kapeldreef 75 B-3001 Leuven Belgium phone: +32-16-281201 fax: +32-16-281515 email: annemie@imec.be WORKSHOP LOCATION ================= Leuven is one of Europe's most ancient university towns, and it is ideally located. The town of Leuven itself came into full bloom a few centuries before the University was founded. Straddling the banks of the then navigable Dijle river and the trade-route from Bruges to the Rhine territories, Leuven grew to become a major trade and textile centre. Leuven was, up to the end of the 13th century, also the residence of the dukes of Brabant. Town and university have known many periods of prosperity. The town hall, churches, cloisters and colleges stand silent witness to those days and make Leuven the interesting place it is. Leuven is only 25 kms away from Brussels, the capital city of Belgium, and the centre of the European Community. The many sites and museums of this important European capital will assure a memorable visit. The centre of Brussels is famous for its Grand Place and the many and varied high quality restaurants in this area cater every purse and taste. It is not by chance that Brussels is now the home of several hundred international organizations. It has become the melting-pot of world thought and culture, with a place in history earned by open and hospitable traditions which have lasted for one thousand years. The workshop will take place in IMEC, the Interuniversity Micro Electronics Center situated at the campus of the Katholieke Universiteit Leuven in Belgium. Access to Leuven ================ a) From Brussels airport By taxi: A taxi takes about 25 minutes from Brussels Airport to Leuven. A single journey will cost about 1800 BEF. Car Rental: Several car rental companies have a desk at Brussels Airport. By Train: There are train connections every 20 minutes. The journey takes about 1 hour to Leuven Railway Station through Brussels North or Central Station. The fare is 200 BEF. Leuven Railway Station is at twenty minutes walk from most of the hotels. A taxi takes about 5 minutes and will cost about 250 BEF. b) If you are not traveling by plane: Leuven can easily be reached by car, since it is situated near a number of main motorways. There are also train connections from Brussels every 30 minutes. WORKSHOP ADDRESS. ================= Address: IMEC, Kapeldreef 75, B-3001 Leuven, Belgium. ============================================================================== Registration Form: Workshop on "Higher Order Logic Theorem Proving and its Applications". September 21-24, 1992, IMEC Leuven Belgium. Please complete this form and return with payment before August 29, 1992. First Name: ____________________________________________________________ Last Name: _____________________________________________________________ Organization: __________________________________________________________ Address: _______________________________________________________________ Postal Code: ___________ City: _________________ Country: _____________ Tel: _________________ Fax: ________________ Email: ___________________ Registration fees: Fee before Fee after 29 August 29 August Full Rate: 13.000 BEF 14.000 BEF _______ Student: 10.000 BEF 11.000 BEF _______ Total: _______ The registration fees include the participation of one person to the workshop, the proceedings, the coffee breaks, the lunches, the workshop banquet and bus transportation between IMEC and the Leuven hotels in the mornings and in the evenings. Please transfer the amount due (in BEF) into bank account nr. 001-1457488-42 (ASLK Bank, Naamsesteenweg, B-3001 Heverlee Belgium) with message "VSDM-DMV HOL92 WORKSHOP". You can also pay with Eurocheque. Payments other than bank transfer in BEF or Eurocheque will entail an extra adminstration charge of 500 BEF. Credit Cards can not be accepted. Hotel Accomodation: =================== Please make your reservation as soon as possible in order to avoid that you will be accomodated in the most convenient way. September is a busy month in Leuven. Indicative prices/night are given for two classes of hotels: Class A (~ 3200 BEF /night) ____ Class B (~ 2200 BEF /night) ____ Arrival Date: __________________ Single Room: ________ Departure Date: __________________ Double Room: ________ Date: _______ Signature: _____________________ Please return this form or a fax to: Annemie Stas, IMEC - Kapeldreef 75 B-3001 Leuven Belgium phone: +32-16-281201 fax: +32-16-281515 email: annemie@imec.be ==============================================================================