Isabelle course -- brief notice

• To: rewriting-list@lorraine.loria.fr, types@dcs.gla.ac.uk, logic@cs.cornell.edu
• Subject: Isabelle course -- brief notice
• From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
• Date: Tue, 07 Feb 1995 16:57:30 +0000
• Approved: types@dcs.gla.ac.uk

INTRODUCTION TO THEOREM PROVING, USING ISABELLE (COURSE)
  12-14 July 1995, Cambridge, England
  Immediately prior to Mathematics of Program Construction (MPC '95).
* Full information available via the WWW page at 
  http://www.cl.cam.ac.uk/users/lcp/isabelle-course.html
* Topics.  The course uses lectures and practical sessions to teach students
  how to use the Isabelle system to perform proofs in higher-order logic.  
  Main points: 
  - Single-step proof checking.  Forward and backward proof.
  - Declaring types and constants.  Quantifier reasoning.  
  - Higher-Order Logic in Isabelle.  Advanced proof tools.
* Lecturer.  Lawrence C Paulson, the originator of Isabelle.
* Cost.  650 pounds sterling (350 pounds for academics) plus accommodation
* Technical Correspondence.  Lawrence C Paulson, Computer Laboratory,
  Pembroke Street, Cambridge CB2 3QG, England.  E-mail lcp@cl.cam.ac.uk
* Adminstrative Correspondence.  The Registration Administrator,
  Programme for Industry, 1 Trumpington St, Cambridge CB2 1QA, England.
  Tel +44 (0)1223 302233.  E-mail: rjs1008@cus.cam.ac.uk

• Prev: LLL : the paper
• Next: Re: Structural Rules and Exponentials
• Index(es):
  • Main
  • Thread