Logic List Mailing Archive

TYPES SUMMER SCHOOL: THEORY AND PRACTICE OF FORMAL PROOFS

TYPES SUMMER SCHOOL: THEORY AND PRACTICE OF FORMAL PROOFS
   September 2-13, 2002, Giens, French Riviera, France
   organized by the the IST European project "TYPES"
   (Computer-Assisted Reasoning based on Type Theory).
   URL: http://www-sop.inria.fr/certilab/types-sum-school02/
 * Scope: 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.
 * Deadline for application: Friday April 19, 2002.