Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 10 Sep 1993 12:18:33 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA27075; Fri, 10 Sep 93 04:12:40 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA27071; Fri, 10 Sep 93 04:12:16 -0700 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 10 Sep 1993 12:12:15 +0100 To: info-hol@cs.uidaho.edu Subject: Isabelle course? Date: Fri, 10 Sep 93 12:12:10 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:133350:930910111218"@cl.cam.ac.uk> I am thinking of running a 3-day Isabelle course next summer, at Cambridge. Details are attached below. If you are *strongly interested* in attending, please let me know and give me your opinion of the proposed date, fee and contents. To avoid cluttering info-hol, please reply directly to me: lcp@cl.cam.ac.uk Larry Paulson Title: Intensive course on generic theorem proving using "Isabelle" Date: Summer 1994 [probably the week before CADE (starting 20 June) or the week after LICS (starting 11 July)] Course fee: 300 pounds (academic), 700 pounds (industrial). Accommodation extra. Isabelle is a theorem prover capable of formal reasoning in many domains. Isabelle has built-in support for several logics, including first-order logic (FOL), higher-order logic (HOL), Zermelo-Fraenkel set theory (ZF) and extensional Contructive Type Theory (CTT). These logics find applications in the areas of hardware/software verification, program synthesis and artificial intelligence. New logics can also be introduced by specifying their abstract syntax, concrete syntax (notation) and inference rules. The course, consisting of lectures and terminal sessions, will enable participants to perform their own Isabelle proofs in higher-order logic. It will be of interest to researchers, academic and industrial, in the fields of computer science and logic. Practical sessions will be conducted on X workstations; participants *must* have experience with such an environment. Participants should also have some experience with formal proof (either on paper or with some other theorem prover). Experience with a functional programming language such as ML would be helpful, but is not essential. Projected course outline: Day 1. single-step proof checking; the simplifier Day 2. some theory; types and type classes; how to make simple definitions Day 3. advanced definitions and new logics; other tools Instructors: L Paulson, S Kalvala, T Nipkow and Ch Prehofer (depends upon number of students) Size: Up to twenty students, with no more than five students per instructor in practical sessions.