EEF Foundations School of Deduction and Theorem Proving (DTP'00)

Heriot-Watt (Edinburgh), April 6-16, 2000

http://www.cedar-forest.org/forest/events/ukiischool2000/ukiischool.html

ULTRA group Useful Logics, Types, Rewriting, and Applications

UKII UK Institute of Informatics, UK

 
 

Preliminary Schedule

http://www.cedar-forest.org/forest/events/ukiischool2000/ukiischool.html
 
 
 

Thursday, 6 April 2000

     13.00 - onwards        REGISTRATION STARTS AND CONTINUES THROUGHOUT SCHOOL

15.00 - 16.00	Tutorial on Proof General David Aspinall
16.00 - 16.30	BREAK
16.30 - 17.30	tutorial on dependently typed records for representing mathematical structure Randy Pollack

9.00 - 10.00	lecture on Algorithmic Proof Nicola Olivetti
10.00 - 10.30	BREAK
10.30 - 11.30	lecture on Algorithmic Proof Nicola Olivetti
11.30 - 12.30	tutorial on Algorithmic Proof Nicola Olivetti

     12.30 - 14.30        LUNCH

14.30 - 15.30	lecture on Explicit Substitutions in (Typed) Lambda Calculi Fairouz Kamareddine
15.30 - 16.00	BREAK
16.00 - 17.00	lecture on syntax for implicit text in formal proofs Stefano Berardi
17.00 - 18.00	tutorial on syntax for implicit text in formal proofs Stefano Berardi

9.00 - 10.00	lecture on Algorithmic Proof Nicola Olivetti
10.00 - 10.30	BREAK
10.30 - 11.30	lecture on Algorithmic Proof Nicola Olivetti
11.30 - 12.30	tutorial on Algorithmic Proof Nicola Olivetti

     12.30 - 14.30        LUNCH

14.30 - 15.30	tutorial on Theorem Proving and Programming with Dynamic First Order Logic Jan van Eijck
15.30 - 16.00	BREAK
16.00 - 17.00	lecture on syntax for implicit text in formal proofs Stefano Berardi
17.00 - 18.00	tutorial on syntax for implicit text in formal proofs Stefano Berardi

                       19.30         SOCIAL BANQUET  
 
 

9.00 - 10.00	lecture on Intersection types: Syntax and Semantics Mariangiola Dezani
10.00 - 10.30	BREAK
10.30 - 11.30	lecture on The Automath System for Verification of Mathematics N.G. de Bruijn
11.30 - 12.30	lecture on The Automath System for Verification of Mathematics N.G. de Bruijn

     12.30 - 14.30        LUNCH

14.30 - 15.30	lecture on Types and Properties of Lambda Terms Mariangiola Dezani
15.30 - 16.00	BREAK
16.00 - 17.00	lecture on The Automath System for Verification of Mathematics N.G. de Bruijn
17.00 - 18.00	lecture on Explicit Reductions and Definitions in (Typed) Lambda Calculi Fairouz Kamareddine

9.00 - 10.00	lecture on Types and Lambda Trees Mariangiola Dezani
10.00 - 10.30	BREAK
10.30 - 11.30	tutorial on The Automath System for Verification of Mathematics N.G. de Bruijn
11.30 - 12.30	lecture on Algorithmic Proof Nicola Olivetti

     12.30 - 14.30        LUNCH

14.30 - 15.15	lecture on Isabelle and Designing a Theorem Prover Larry Paulson
15.15 - 15.45	BREAK
15.45 - 16.30	lecture on Isabelle and Designing a Theorem Prover Larry Paulson
16.30 - 18.00	tutorials and practicals on Isabelle Jacques Fleuriot

                       19.30         SOCIAL BANQUET  
 
 

9.00 - 9.45	lecture on Isabelle and Designing a Theorem Prover Larry Paulson
9.45 - 10.15	BREAK
10.15 - 11.00	lecture on Isabelle and Designing a Theorem Prover Larry Paulson
11.00 - 12.30	tutorial on Isabelle and Designing a Theorem Prover Jacques Fleuriot

     12.30 - 14.30        LUNCH

14.30 - 16.00	practicals on Isabelle Jacques Fleuriot
16.00 - 16.30	BREAK
16.30 - 18.00	practicals on Isabelle Jacques Fleuriot

9.00 - 10.00	lecture on Modal and Temporal Logics Colin Stirling
10.00 - 10.30	BREAK
10.30 - 11.30	lecture on Modal and Temporal Logics Colin Stirling
11.30 - 12.30	tutorial on Modal and Temporal Logics Colin Stirling

     12.30 - 14.30        LUNCH

14.30 - 15.30	lecture on Types in Logic, Mathematics and Programming Robert Constable
15.30 - 16.00	BREAK
16.00 - 17.00	lecture on Types in Logic, Mathematics and Programming Robert Constable
17.00 - 18.00	lecture on Coq Daniel Hirschkoff

9.00 - 10.00	lecture on Coq Daniel Hirschkoff
10.00 - 10.30	BREAK
10.30 - 11.30	lecture on Types in Logic, Mathematics and Programming Bob Constable
11.30 - 12.30	lecture on Coq Daniel Hirschkoff

     12.30 - 14.30        LUNCH

14.30 - 15.30	lecture on Coq Daniel Hirschkoff
15.30 - 16.00	BREAK
16.00 - 18.00	practicals on Coq Daniel Hirschkoff

                       19.30         SOCIAL BANQUET  
 
 

9.00 - 10.00	lecture on Algorithmic Proof Nicola Olivetti
10.00 - 10.30	BREAK
10.30 - 12.30	practical on Coq Daniel Hirschkoff

     12.30 - 14.30        LUNCH

14.30 - 15.30	lecture on Computation and deductions by rewriting with ELAN Claude Kirchner
15.30 - 16.00	BREAK
16.00 - 17.00	lecture on Computation and deductions by rewriting with ELAN Claude Kirchner
17.00 - 18.00	tutorial on Computation and deductions by rewriting with ELAN Claude Kirchner

9.00 - 10.00	lecture on Computation and deductions by rewriting with ELAN Claude Kirchner
10.00 - 10.30	BREAK
10.30 - 11.30	tutorial on Computation and deductions by rewriting with ELAN Claude Kirchner

                       12.00          END  of DTP'00