Types summer school'02: Theory and practice of formal proofs

Giens, France, September 2-13, 2002

Program

The program will consist of four parts:
  • Introduction and Background (9 hours):
  • Benjamin Werner, Inria: Proofs, Proof development, Logic, and Lambda-calculus
  • Herman Geuvers, Nijmegen: Pure Type Systems
  • Thierry Coquand, Chalmers: Inductive Definitions in Programming Languages and Type Theory

  • Systems (14 hours):
    - An overview of the two proof assistants to be used in the course, including short developments of proofs (6h):
  • The Logical team, Inria: The Coq system
  • Tobias Nipkow, München: The Isabelle/HOL system
    • - A few other systems and man-machine interfaces (8h):
  • Paul Callaghan, Durham: Plastic
  • Catarina Coquand, Chalmers: Agda
  • Christophe Raffalli, Chambery: PhoX
  • Carsten Schuermann, Yale: Twelf
  • Laurent Théry, Inria: A quick overview of PVS and HOL
  • David Aspinall, Edinburgh: Proof General: a general man-machine interface for proof assistants
  • Yves Bertot, Inria: PCoq, a man-machine interface dedicated to Coq

  • Advanced Topics (13 hours):
  • Per Martin-Löf, Stockholm: Informal Semantics of Type Theory
  • Peter Dybjer, Chalmers: Dependant Types in Programming
  • Susanne Graf, Verimag: Model Checking, Abstractions
  • Gregory Morrisett, Cornell : Proof-Carrying Code
  • Davide Sangiorgi, Inria: Types for Mobile Process

  • Applications (9 hours):
  • Martin Abadi, UCSC: Security
  • Paul Jackson, Edinburgh: Hardware Verification
  • Laurent Théry, Inria: Formalised Mathematics
    • In addition to this, there will be a couple of hours reserved for lab work on the computers each day, under the supervision of the lecturers who have presented the systems (total: 14 hours).
    The lab will be open every evening and during the week-end; Participants will get a real oportunity to experiment the systems presented in the course.

    Registration: on Sunday September 1st after dinner, from 9:00pm to 10:30pm, and on Monday September 2nd from 8:15am to 9:00am and from 11:00am to 11:30am.

    First week (September 2 - 7)

    Monday 2 Tuesday 3 Wednesday 4 Thursday 5 Friday 6 Saturday 7
    9:00 - 10:00
    10:00 - 11:00
    11:00 - 11:30
    11:30 - 12:30
    12:30 - 2:30
    2:30 - 3:30
    3:30 - 4:00
    4:00 - 5:00
    5:00 - 6:30
    8:00 - 9:00
    		Werner
    Werner
    coffee
    Werner
    -- lunch --
    Coq
    coffee
    Coq; Proof-Gen
    lab
    -- dinner --     		Geuvers
    Geuvers
    coffee
    Coquand
    -- lunch --
    Coq; PCoq
    coffee
    lab
    lab
    -- dinner --     		Coquand
    Coquand
    coffee
    Geuvers
    -- lunch --




    -- dinner --     		Dybjer
    Dybjer
    coffee
    Coq
    -- lunch --
    Isabelle
    coffee
    Isabelle
    lab
    -- dinner --     		Abadi
    Abadi
    coffee
    Plastic
    -- lunch --
    Isabelle
    coffee
    lab
    lab
    -- dinner --     		Martin-Löf
    Martin-Löf
    coffee
    Abadi
    -- lunch --




    -- dinner --

    Social Event: An excursion will be organized to the Porquerolles Island on Sunday September 8th, from 10:30am to 5:30pm (exact time to be confirmed). Dinner is from 8:00pm to 9:00pm as usual.

    Second week (September 9 - 13)

    Monday 9 Tuesday 10 Wednesday 11 Thursday 12 Friday 13
    9:00 - 10:00
    10:00 - 11:00
    11:00 - 11:30
    11:30 - 12:30
    12:30 - 2:30
    2:30 - 3:30
    3:30 - 4:00
    4:00 - 5:00
    5:00 - 6:30
    8:00 - 9:00
    		Théry
    Théry
    coffee
    Agda
    -- lunch --
    Agda
    coffee
    lab
    lab
    -- dinner --     		Morrisett
    Morrisett
    coffee
    Jackson
    -- lunch --
    Twelf
    coffee
    PhoX
    lab
    -- dinner --     		Jackson
    Jackson
    coffee
    Morrisett
    -- lunch --




    -- dinner --     		Sangiorgi
    Sangiorgi
    coffee
    Sangiorgi
    -- lunch --
    pvs & hol
    coffee
    pvs & hol
    lab
    -- dinner --     		Graf
    Graf
    coffee
    Graf
    -- lunch --
    lab
    coffee


    -- dinner --

    On Wednesday and/or Saturday afternoon, you might go and visit the famous little village of Saint-Tropez, for example, not far from Giens, by bus or by car.