Atlas home || Conferences | Abstracts | about Atlas
Host: Esprit working group 21900 - TYPES
Homepage: http://www-sop.inria.fr/croap/personnel/Joelle.Despeyroux/types-sum-school.html
Organizers: Joëlle Despeyroux, Monique Simonetti
Description:
During the last few years major achievements have been made in using computers for interactive proof developments to produce secure software.
This two weeks' course is for postgraduate students, researchers and industrials who want to learn about interactive proof development. There will be introductory
and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, and other topics which give relevant theoretical background.
Several talks will be devoted to the presentation of applications.
The proof assistants presented in the school represent the current state-of-the-art in interactive theorem proving. Participants will get extensive opportunities to use
the systems in a workstation environment for developing their own proofs.
Date received: February 06, 1999
© 2008 Atlas Conferences Inc.