- From: Bengt Nordström <bengt@cs.chalmers.se>
- Date: Fri, 25 Feb 2005 13:46:17 +0100
- To: types@lists.chalmers.se
- Cc: appsem@appsem.org, types@cis.upenn.edu, categories@mta.ca, eapls@jiscmail.ac.uk, eacsl@dimi.uniud.it, eatcs-it@cs.unibo.it, acl2@cs.utexas.edu, calculemus-ig@ags.uni-sb.de, caml-list@inria.fr, comlab@comlab.ox.ac.uk, compulog-deduction@cs.bham.ac.uk, coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk, lfcs-interest@dcs.ed.ac.uk, members@fmeurope.org, mizar-forum@mizar.uwb.edu.pl, nqthm-users@cs.utexas.edu, nuprllist@cs.cornell.edu, projects-mkm-ig@iu-bremen.de, pvs@csl.sri.com, zforum@prg.ox.ac.uk, www-math@w3.org
Proofs of Programs and Formalisation of Mathematics
August 15-26 2005, Goteborg, Sweden
http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/
During the last ten years major achievements have been made in using
computers for interactive proof developments to produce secure
software and to show interesting mathematical results. Recent major
results are, for instance, the complete formalisation of a proof of
the four colour theorem, and a formalisation of the prime number
theorem.
This two weeks' course is for postgraduate students, researchers and
industrials who want to learn about interactive proof development.
The present school follows the format of previous TYPES summer school
(in Baastad 1993, Giens 1999, Giens 2002). There will be introductory
and advanced lectures on lambda calculus, type theory, logical
frameworks, program extraction, and other topics with relevant
theoretical background. Several talks will be devoted to
applications.
During these two weeks we will present three proof assistants: Coq,
Isabelle and Agda, which are state-of-the-art interactive theorem
provers. Participants will get extensive opportunities to use the
systems for developing their own proofs. No previous knowledge of
type theory and lambda calculus is required.
The school is organised by the TYPES working group "Types for Proofs
and Programs", which is a project in the IST (Information Society
Technologies) program of the European Union. A limited number of grants
covering part of travel, fees and ackommodation are available. Neither
participation nor grants are restricted to TYPES participants.
Lecturers:
---------
Jeremy Avigad, Carnegie-Mellon Connor McBride, Nottingham
Yves Bertot, INRIA Sophia Alexandre Miquel, Paris 7
Thierry Coquand, Chalmers Tobias Nipkow, TU Munich
Catarina Coquand, Chalmers Bengt Nordstrom, Chalmers
Gilles Dowek, INRIA Futurs Erik Palmgren, Uppsala
Peter Dybjer, Chalmers Christine Paulin, Paris Sud
Herman Geuvers, Nijmegen Laurent Thery, INRIA Sophia
John Harrison, INTEL Freek Wiedijk, Nijmegen
Per Martin-Lof, Stockholm
TENTATIVE PROGRAM
-----------------
Introduction to Type Theory:
Lambda-calculus
Propositions-as-types
Inductive sets and families of sets
Predicative and non-predicative theories
Foundations:
Introduction to Systems:
Coq
Isabelle
Agda
Advanced applications and tools:
Proving properties of Java programs
Reasoning about Programming Languages
Coinduction
Correctness of floating-point algorithms
Dependently typed programming:
Dependently typed datastructures
Compiling dependent types
Formalisation of mathematics:
Introduction
Fundamental theorem of algebra
Bishop' set theory
Other examples, e.g. prime number theorem
The organising committee: Andreas Abel, Ana Bove, Catarina Coquand,
Thierry Coquand, Peter Dybjer and Bengt Nordstrom.
Received on Saturday, 26 February 2005 06:10:26 UTC