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

Giens, France, August 30 - September 10, 1999

Program

The program will consist of four parts:
  • Introduction and background:
  • Henk Barendregt: The quest for correctness
  • Bengt Nordström: Representing proofs and statements
  • Herman Geuvers: Pure Type Systems
  • Thierry Coquand: Inductive definitions and Type Theory
  • Systems:
    (An overview of each of the four proof assistants to be used in the course, including some short developments of actual proofs)
  • Benjamin Werner: The Coq system
  • Zhaohui Luo: The Lego system
  • Catarina Coquand and Thomas Hallgren: Agda, the current version of the Alf family
  • Tobias Nipkow: The Isabelle system
  • Avanced topics:
  • Per Martin-Löf: Nonstandard Type Theory
  • Michel Parigot: Program extraction in 2nd order classical logic
  • Laurent Théry: A quick overview of PVS and HOL
  • Jean-Louis Krivine: Lambda-calculus and ZF
  • Stefano Berardi: Types and program optimization
  • Yves Lafont: Linear logic and computer science
  • Applications:
  • John Harrison: Formal verification in industry
  • Henrik Persson: Certified computer algebra
  • Jaco van de Pol: Proofs of correctness of protocols
  • Tobias Nipkow: Formalizing and analyzing Java in Isabelle/HOL
  • Aarne Ranta: Linguistic applications of type theory
    • In addition to this, there will be several hours reserved for lab work on the computers each day.

    Registration: on Sunday August 29th from 9:00pm to 10:00pm, and on Monday August 30th from 8:15am to 9:00am and from 11:00am to 11:30am.

    First week (August 30 - September 4)

    Monday Tuesday Wednesday Thursday Friday Saturday
    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
    		Barendregt
    Barendregt
    coffee
    Nordström
    LUNCH
    Coq
    coffee
    Coq
    lab
    DINNER     		Geuvers
    Geuvers
    coffee
    Coquand
    LUNCH
    Coq
    coffee
    lab
    lab
    DINNER     		Coquand
    Coquand
    coffee
    Coq
    LUNCH




    DINNER     		Martin-Löf
    Martin-Löf
    coffee
    Lego
    LUNCH
    Lego
    coffee
    lab
    lab
    DINNER     		Parigot
    Parigot
    coffee
    Agda
    LUNCH
    Théry
    coffee
    Agda
    lab
    DINNER     		Théry
    Harrison
    coffee
    Harrison
    LUNCH




    DINNER

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

    Second week (September 6 - 10)

    Monday Tuesday Wednesday Thursday Friday
    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 - 6:30
    8:00 - 9:00
    		Persson
    Persson
    coffee
    Agda
    LUNCH
    Agda
    coffee
    lab
    DINNER     		Krivine
    Krivine
    coffee
    Isabelle
    LUNCH
    Isabelle
    coffee
    lab
    DINNER     		Berardi
    Berardi
    coffee
    van de Pol
    LUNCH



    DINNER     		Nipkow
    Nipkow
    coffee
    Ranta
    LUNCH
    Ranta
    coffee
    lab
    DINNER     		Lafont
    Lafont
    coffee
    van de Pol
    LUNCH
    lab
    coffee

    DINNER