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; Wed, 20 Apr 1994 18:10:32 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA21947; Wed, 20 Apr 1994 10:39:00 -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 AA21939; Wed, 20 Apr 1994 10:37:12 -0600 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA19662; Wed, 20 Apr 1994 09:36:56 -0700 Received: from albatross.cl.cam.ac.uk (user adg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 20 Apr 1994 17:33:23 +0100 To: weigert@comm.mot.com (Thomas Weigert) Cc: info-hol@cs.uidaho.edu Subject: Re: HOL class In-Reply-To: Your message of "Wed, 20 Apr 94 10:34:11 CDT." <9404201534.AA06692@weinberg> Date: Wed, 20 Apr 94 17:33:09 +0100 From: Andrew Gordon Message-Id: <"swan.cl.cam.:258280:940420163327"@cl.cam.ac.uk> >Has anyone heard of any plans of a summer school (or similar class) on HOL >or any of the other similar theorem proving frameworks? Any hints are >appreciated. I see that Gerard Huet will be lecturing on Coq at the Udine summer school this September. Like HOL, Coq is an interactive theorem prover for a higher-order logic, although the nature of both the interaction and the logic is different from HOL. I'm not a Coq user myself, but I gather that if you want to do proofs about functional programs it's a pretty nifty environment. Andy. PRELIMINARY ANNOUNCEMENT ADVANCED SCHOOL ON TYPED LAMBDA CALCULUS AND FUNCTIONAL PROGRAMMING September 19 - September 30, 1994 CISM, Palazzo del Torso, Piazza Garibaldi, 18 - UDINE Udine (ITALY) The Advanced School is organized under the auspices of the Italian Chapter of EATCS (European Association for Theoretical Computer Science) and UNESCO. It is supported also by the University of Udine and the CNR. Formal Methods for specifying, modularizing, verifying, and reusing large programs and systems, as well as principled languages, which allow to apply rapidly such methods, are greatly needed in Computer Science. Typed Lambda Calculus has been recently understood as a central node in a conceptual network which links various fields of Logic to Computer Science. It has made possible to transfer fruitfully ideas and techniques from Category Theory, Proof Theory, Type Theory to Computer Science. Based on formally solid and conceptually disciplined logical grounds, Typed Lambda Calculus allows for the development of a mathematically clear style of programming as well as for the design of flexible logical tools and methods for Computer Science. In recent years, Typed Lambda Calculus has been impressively used also as a metalanguage for defining formal systems for reasoning about Programs and as a logical framework for designing interactive proof assistants} for computer aided formal reasoning. The School will offer 5 series of (approx.8-10) introductory and advanced lectures on the connections between Typed Lambda Calculus and Category Theory, Proof Theory, and Type Theory, and on the, more recent, applications of Typed Lambda Calculus, such as the design of Typed Functional Languages, General Proof Assistants, and Program Logics. SCHOOL DIRECTORS M. DEZANI CIANCAGLINI (Torino) FURIO HONSELL (Udine) LIST OF SPEAKERS JEAN-YVES GIRARD (Marseilles) Proof Theoretic Foundations GERARD HUET (INRIA Rocquencourt) Advanced Typed Functional Languages: Theorem Proving in Coq JOHN MITCHELL (Stanford) Type Systems and Programming Languages EUGENIO MOGGI (Genova) Meta-languages and Applications S. RONCHI DELLA ROCCA (Torino) Basic Lambda Calculus The School is intended primarily for young researchers and PhD students in Computer Science and Mathematics. During the School, participants will be able to attend also informal talks and discussions of open problems. PhD students may ask to sit for an examination at the School. It will consist of a Seminar on a topic agreed upon by the Directors and the Speakers. There will be demonstrations, and participants will have the opportunity to use a computer environment. To apply, participants should fill the form (to be publicized shortly) and return it together with a recommandation letter to: Advanced School Secretariat: Professor F.Honsell Universita' di Udine, Dipartimento di Matematica e Informatica via Zanon, 6, 33100 UDINE - ITALY Tel: 39-432-272220 Fax: 39-432-510755 The DEADLINE for application is July 31st 1994. Further information can be obtained via email under the address: scuola@dimi.uniud.it FEES and SCHOLARSHIPS The participation fee is 650.000 Italian Liras. There is a limited number of scholarships available for people who cannot obtain funding for their travel, participation fee and living expenses from their institutions. A request for full or partial support should be enclosed with the applications.