Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 1 Jul 1994 16:39:45 +0100 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA24969 for qed-out; Fri, 1 Jul 1994 10:23:57 -0500 Received: from vanuata.dcs.gla.ac.uk (vanuata.dcs.gla.ac.uk [130.209.240.50]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA24955 for ; Fri, 1 Jul 1994 10:23:37 -0500 From: hug94@dcs.gla.ac.uk Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk with LOCAL SMTP (PP) id <04543-0@goggins.dcs.gla.ac.uk>; Fri, 1 Jul 1994 16:23:23 +0100 Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA03233; Fri, 1 Jul 94 16:23:21 BST Message-Id: <9407011523.AA03233@switha.dcs.gla.ac.uk> To: qed@mcs.anl.gov Cc: hug94@dcs.gla.ac.uk Subject: HOL'94 - Second Call for Participation. Date: Fri, 01 Jul 94 16:23:20 +0100 Sender: owner-qed@mcs.anl.gov Precedence: bulk Attached is the programme and registration information for the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, to be held in Malta, 19-22 September 1994. See also http://www.dcs.glasgow.ac.uk/~hug94 for further information. Please accept my apologies for any multiple copies due to overlapping mailing lists. Tom Melham Programme Chair HOL'94 (Malta) ========================================================================= REGISTRATION AND PROGRAMME INFORMATION ------------------------------------------------------------------------- HOL 1994 INTERNATIONAL CONFERENCE ON HIGHER ORDER LOGIC THEOREM PROVING AND ITS APPLICATIONS MALTA 19-22 SEPTEMBER 1994 University of Malta -------------------------------------------------------------------------- SPONSORED BY BANK OF VALLETTA MALTA'S LEADING BANK ========================================================================== OBJECTIVES This meeting is the seventh in a series of annual workshops on higher order logic theorem proving and its applications, with a primary focus on the HOL system and similar systems. Previous workshops were held in Cambridge, Aarhus, Davis, Leuven, and Vancouver. Mechanized theorem provers for higher order logic have been applied to many areas, including design and verification, security, real-time systems, semantics, compiler verification, program correctness, concurrency, and program refinement. The theorem proving technology itself is also an active area of research. This conference will bring together researchers in these and related areas of investigation for the dissemination and discussion of new developments in the field. THE CONFERENCE The Conference, which will be held in Malta between the 19-22 September, 1994 will consist of morning and afternoon sessions during which invited papers and refereed papers will be presented and discussed. Formal proceedings will be published by Springer Verlag in the Lecture Notes in Computer Science Series. Papers discussing work in progress will also be presented, and will be circulated in an informal participants' proceedings. The Organising Committee has invited the following guest speakers: o Prof. Dr. N.G. de Bruijn (Eindhoven) "Highlighting the Lambda-free Fragment of Automath" o Dr. Thomas Forster (Cambridge) "Weak Systems of Set Theory Related to HOL" o Dr. Keith Hanna (Kent) "Reasoning about Real Circuits" THE VENUE The University of Malta is one of the oldest in Europe, owing its origin to the Collegium Melitense founded by the Jesuits in 1592. A new campus at Msida was opened during the Independence celebrations in 1964, to provide for the future growth and needs of higher education in Malta. The Conference will be held at the Foundation for International Studies which is housed in the original premises of the Collegium Melitense. Malta is well connected to all the major European and North African airports. London - Malta is a three hour flight and costs approximately US $350. Frankfurt or Paris to Malta are two hour flights in a similar price range to the London flight. Rome-Malta is a one hour flight and should not cost more than US $230. Those coming to Malta from outside Europe can do so via any major airport in Europe, although London often proves easier and cheaper. The average temperature in Malta in September is 30 degrees celcius. THE ORGANISERS Programme Chair: Thomas Melham (Glasgow) Programme Committee: Flemming Andersen (TDR), Richard Boulton (Cambridge), Shui-Kai Chin (Syracuse), Elsa Gunter (AT&T), John Herbert (SRI), Jeffrey Joyce (UBC), Gilles Kahn(INRIA), Ramayya Kumar (FZI), Tim Leonard (DEC), Karl Levitt (UC Davis), Paul Loewenstein (SUN), Tom Schubert (Portland State), David Shepherd (INMOS), Joakim von Wright (SHH), Phil Windley (BYU). PAPERS Category A papers: LCF Examples in HOL Sten Agerholm A Graphical Tool for Proving UNITY Progress Flemming Andersen, Kim Dam Petersen, and Jimmi S. Pettersson Reasoning About a Class of Linear Systems of Equations in HOL Catia M. Angelo, Luc Claesen, and Hugo De Man Towards a HOL theory of memory J-P. Bodeveix, M. Filali, and P. Roche Providing Tractable Security Analyses in HOL Stephen H. Brackin First-Order Automation for Higher-Order-Logic Theorem Proving Holger Busch Symbolic Animation as a Proof Tool Juanito Camilleri and Vincent Zammit Datatypes in L2 Nick Chapman, Simon Finn, and Michael P. Fourman A Formal Theory of Undirected Graphs in Higher-Order Logic Ching-Tsun Chou Mechanical Verification of Distributed Algorithms in Higher-Order Logic Ching-Tsun Chou Tracking Design Changes with Formal Verification Paul Curzon Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circuit Behavior David A. Fura and Arun K. Somani An Interpretation of NODEN in HOL Brian T. Graham Binary Decision Diagrams as a HOL Derived Rule John Harrison Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator Peter V. Homeier and David F. Martin S : A Machine Readable Specification Notation based on Higher Order Logic J. Joyce, N. Day, and M. Donat An Engineering Approach to Formal Digital System Design Mats Larsson Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics Juin-Yeu Lu and Shiu-Kai Chin 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 Towards a Mechanically Supported and Compositional Calculus to Design Distributed Algorithms I.S.W.B. Prasetya 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 A Parameterized Proof Manager Konrad Slind Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL Sofi\`{e}ne Tahar and Ramayya Kumar Specifying Instruction-Set Architectures in HOL: A Primer Phillip J. Windley Representing higher-order logic proofs in HOL J. von Wright Category B papers: Formal Reasoning about Specification and Transformation of Reactive Systems J\"{u}rgen Bohn A Higher-order Theory of Lists for HOL Paul Curzon, Wai Wong Evaluation Techniques as a Part of the Verification Process Dirk Eisenbiegler and Ramayya Kumar A Interpreter Interface Language and Its Formal Embedding in Higher-Order Logic David A. Fura and Arun K. Somani Not Implementing N-Bit Words by Using Abstract Theories Kelly M. Hall and Phillip J. Windley A Reference Version of HOL John Harrison and Konrad Slind Trustworthy Tools for Trustworthy Programs: Automatic Verification of Mutually Recursive Procedures Peter V. Homeier and David F. Martin Why Hardware Verification Needs more than Model Checking Klaus Schneider, Ramayya Kumar, Thomas Kropf A Tree-Based, Graphical Interface for Large Proof Development Tom Schubert and John Biggs Towards Efficient Conversions by use of Partial Evaluation Morten Welinder Using Make to Manage Large Proofs Phillip J. Windley Towards a Formal Verification of a Secure and Distributed System and Applications Zhang, Shaw, Heckman, Benson, Beard, Archer, Levitt, Olsson ===================================================================== Administration Address HOL'94 Room 202, First Floor, New Computer Building,University of Malta, Tal-Qroqq, Msida, Malta MSD06 Tel: + 356 346674 Fax: + 356 320539 e-mail: hug94@unimt.mt or hug94@dcs.gla.ac.uk Conference Chair: Juanito Camilleri (Malta) --------------------------------------------------------------------- REGISTRATION INFORMATION The conference fee is: Lm 85 US $223 UK pounds 145 Student rate: Lm 60 US $156 UK pounds 102 The fee covers: # Registration for the Conference # Conference proceedings # Coffee/tea during morning and afternoon breaks # Lunch # Conference dinner Applications for registration on the attached form, together with payment of the registration fee, should be sent to the address given below to arrive not later than 15th August, 1994. All administrative correspondence should be addressed to the organisers at: HOL'94 Room 202, First Floor, New Computer Building, University of Malta, Tal-Qroqq, Msida, Malta MSD06 Tel: + 356 346674 Fax: + 356 320539 e-mail: hug94@unimt.mt or hug94@dcs.gla.ac.uk --------------------------------------------------------------------- ACCOMODATION* We have reserved a limited number of rooms at the following hotels: # The Diplomat (4-star Hotel) Single Occupancy US$41 UK pounds 27 Twin Room Sharing US$36 UK pounds 23 # Milano Due (3-Star Hotel) Single Occupancy US$38 UK pounds 25 Twin Room Sharing US$30 UK pounds 20 Those who would like to book accommodation through us are kindly requested to return their accommodation forms to the respective hotels to arrive by not later than 30th July, 1994. Please keep in mind that September falls during Malta's peak tourist season and it will be extremely difficult to find accommodation in August and September. Prospective participants are kindly encouraged to apply as early as possible as bookings for accommodation will be taken on a first- come first-served basis. Late requests for accommodation should go to the relevant hotel, but cannot be guaranteed. * All rates for accommodation are per person per night. Prices are inclusive of 5% Govt levy. -- cut here ---------------------------------------------------------------- REGISTRATION FORM Title______________________ First Name________________________________ Surname________________________________________________________________ Job Title______________________________________________________________ Organisation___________________________________________________________ Address________________________________________________________________ _______________________________________________________________________ City______________________________________Postcode ____________________ Country_______________________________ Tel _________________________ Fax___________________________________ e-mail_______________________ Do you have any special dietary or medical requirements? ____ YES ____ NO If yes, please specify _____________________________________________________________________ _____________________________________________________________________ ____ Cheque enclosed made payable to University of Malta (HOL '94) ____ Bank Draft to: University of Malta (HOL '94), Account No: 852 873 329 ____ Please charge my Mastercard / Visa / Diners / Cirrus with US$ _______________ / UK pounds ________________ Card Number _________________________________________________ Expiry Date: __ __ / __ __ /__ __ Signature of Cardholder _____________________________________ I confirm that I have read and agree to the conditions of registration as specified in the information section. Signed _____________________ Date ______________ Please complete the Registration Form IN INK and return it to the administration address. Please note that your registration can only be accepted if accompanied by payment for the amount due as Conference Fee. Payments should be effected by not later than 15th August, 1994. The organising committee regrets that it cannot refund any payment in case of cancellation. -- cut here ---------------------------------------------------------------- ACCOMMODATION BOOKING FORM (FOUR STAR HOTEL) The Diplomat Hotel* Tower Road, Sliema SLM16, Malta Tel:+356 345361/6 Fax:+356 345351 Single Occupancy US$41 UK pounds 27 _____ Twin Room Sharing US$36 UK pounds 23 _____ Title_________ First Name_______________________________________ Surname___________________________________________________________ Job Title_________________________________________________________ Organisation______________________________________________________ Address___________________________________________________________ __________________________________________________________________ City_______________________________ Postcode____________________ Country____________________________ Tel________________________________ Fax_________________________ e-mail_____________________________ No. of Accompanying Persons_______________________________________ If sharing with another participant, please state name of person so as to avoid duplicate reservations __________________________________________________________________ Date Flight Number & Time of Arrival Arrival __________ ______________________________ Departure __________ ______________________________ _____ Please find enclosed cheque/bank draft for US$______ / UK pounds______ made payable to The Diplomat Hotel _____ Please charge my Mastercard / Visa / Diners / Cirrus with US$ _______________ / UK pounds ________________ Card Number ___________________________________ Expiry Date: __ __ / __ __ / __ __ Signature of Cardholder___________________________ Please complete this booking from IN INK and return to the hotel above. Please note that your booking can only be accepted if paid in full through one of the methods listed above. Payments should be effected to arrive by not later than 30th July, 1994. * Accommodation includes breakfast and all rates are per person per night. Prices are inclusive of 5% Govt levy. -- cut here ---------------------------------------------------------------- ACCOMMODATION BOOKING FORM (THREE STAR HOTEL) Hotel Milano Due The Strand, Gzira Tel: +356 345040-4 or 343112-4 Fax: +356 345045 Single Occupancy US$38 UK pounds 25 ________ Twin Room Sharing US$30 UK pounds 20 ________ Title___________ First Name______________________________________ Surname___________________________________________________________ Job Title_________________________________________________________ Organisation______________________________________________________ Address___________________________________________________________ __________________________________________________________________ City_______________________________ Postcode____________________ Country____________________________ Tel________________________________ Fax_________________________ e-mail_____________________________ No. of Accompanying Persons__________________________ If sharing with another participant, please state name of person so as to avoid duplicate reservations __________________________________________________________________ Date Flight Number & Time of Arrival Arrival __________ __________________________ Departure __________ ________________________ _____ Please find enclosed cheque/bank draft for US$______/UK pounds_____ made payable to Hotel Milano Due _____ Please charge my Mastercard / Visa / Diners / Cirrus with US$ _______________ / UK pounds ________________ Card Number ___________________________________ Expiry Date: __ __ / __ __ /__ __ Signature of Cardholder___________________________ Please complete this booking from IN INK and return to the hotel above. Please note that your booking can only be accepted if paid in full through one of the methods listed above. Payments should be effected to arrive by not later than 30th July, 1994. * Accommodation includes breakfast and all rates are per person per night. Prices are inclusive of 5% Govt levy. =====================================================================