EEF Foundations school in Deduction and Theorem Proving
Heriot-Watt University, Edinburgh, 6-16 April, 2000
Useful Logics, Types, Rewriting,
UK Institute of Informatics,
PG Manual Excerpt
by Aspinall, Goguen, Kleymann and Seqeira.
What is proof general?
The type theory and type checker of GF
by Maenpaa and Ranta.
: Intersection Types. See in particular
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. See
: Explicit Extensions in Typed Lambda calculi. See
: Types in Logic, Mathematics and Programming. See:
Nuprl's Class Theory and its Applications
. by Constable and Hickey
The Nuprl Open Logical environment (to be scanned, so far only in hard copy). By Allen, Constable, Eaton, Kreitz and Lorigo.
Proof Translation Study (to be scanned, so far only in hard copy).
Isabelle HOL, the tutorial
by Tobias Nipkow.
Lecture 2: Theory Files
Lecture 3: Inteative proof
Lecture 4: The Mutilated Chess Board
. See in particular
by Huet, Kahn and Paulin-Mohring.
N.G. de Bruijn: The AUTOMATH System for verification of Mathematics. (to be scanned, so far only in hard copy).
Jan van Eijck
: Tableaux Theorem Proving for Dynamic First Order Logic. See
by van Eijck, Heguiabehere and O' Nuallain
Logic, Rewriting and Deduction:
: Elan and Deduction Modulo.
What is rewriting?
Introduction to ELAN and the rewrite calculus
Deduction Modulo: Concepts, Mechanisation, Applications
: Algorithmic Proof theory. See
by Gabbay and Olivetti
Colin Stirling: Modal Logics for Processes. See
by Bradfield and Stirling.