EEF Foundations school in Deduction and Theorem Proving

Heriot-Watt University, Edinburgh, 6-16 April, 2000

ULTRA group Useful Logics, Types, Rewriting, and Applications

UKII UK Institute of Informatics, UK

• Announcement of school
• Travel Information
• Table of Contents
• Program
• Lecture Notes
• PG Manual Excerpt by Aspinall, Goguen, Kleymann and Seqeira.
• What is proof general? by Aspinall.
• The type theory and type checker of GF by Maenpaa and Ranta.
• Intersection Types for lambda trees by van Bakel, Barbanera, Dezani and de Vries.
• A complete carachterisation of the complete intersection type theories by Alessi, Dezani and Honsell.
• Intersection Types in programming Languages by Joe Wells.
• Explicit Extensions in Typed Lambda calculi by Fairouz Kamareddine.
• Nuprl's Class Theory and its Applications. by Constable and Hickey
• The Nuprl Open Logical environment, by Allen, Constable, Eaton, Kreitz and Lorigo.
• Proof Translation Study by the Nuprl group.
• Isabelle HOL, the tutorial by Tobias Nipkow.
• Lecture 1:Tour by Larry Paulson.
• Lecture 2: Theory Files by Larry Paulson.
• Lecture 3: Inteative proof by Larry Paulson.
• Lecture 4: The Mutilated Chess Board by Larry Paulson.
• The Coq proof Assistant, a tutorial by Huet, Kahn and Paulin-Mohring.
• The AUTOMATH System for verification of Mathematics by de Bruijn
• Tableaux Theorem Proving for Dynamic First Order Logic by van Eijck, Heguiabehere and O' Nuallain
• What is rewriting? by Claude Kirchner.
• Introduction to ELAN and the rewrite calculus by Claude Kirchner.
• Deduction Modulo: Concepts, Mechanisation, Applications by Claude Kirchner.
• Algorithmic Proof theory by Gabbay and Olivetti
• Modal Logics for Processes by Bradfield and Stirling.
• photos from the school by fairouz Kamareddine
• photos from the school by Jurgen Stueber
• photos from the school by Yoko Motohama
• photos by Marko Kaaramees.