home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / specific / 626 < prev    next >
Encoding:
Internet Message Format  |  1993-01-21  |  2.8 KB
  1. Path: sparky!uunet!paladin.american.edu!howland.reston.ans.net!spool.mu.edu!enterpoop.mit.edu!eru.mt.luth.se!lunic!sunic!chalmers.se!cs.chalmers.se!augustss
  2. From: augustss@cs.chalmers.se (Lennart Augustsson)
  3. Newsgroups: comp.specification
  4. Subject: Summer School: TYPES FOR PROOFS AND PROGRAMS
  5. Message-ID: <1993Jan21.155346.19643@cs.chalmers.se>
  6. Date: 21 Jan 93 15:53:46 GMT
  7. Sender: news@cs.chalmers.se (News administrator)
  8. Reply-To: baastad@cs.chalmers.se
  9. Organization: Dept. of CS, Chalmers, Sweden
  10. Lines: 78
  11.  
  12.  
  13.              INTERNATIONAL SUMMER SCHOOL
  14.  
  15.                       ON
  16.  
  17.             TYPES FOR PROOFS AND PROGRAMS
  18.  
  19.               BAASTAD, SWEDEN, JUNE 7 - 18, 1993
  20.  
  21.  
  22. During the last few years major achievements have been made in using
  23. computers for interactive proof developments. Several proof assistants
  24. (such as Coq, Lego, and Alf) have been developed based on the idea of
  25. a logical framework in which it is possible to define a variety of
  26. logics. Many quite substantial proofs from mathematics, logic, and
  27. computing have also been implemented in them.
  28.  
  29. This two week course is for postgraduate students and researchers who
  30. want to learn about interactive proof development. There will be
  31. introductory and advanced lectures on lambda calculus, type theory,
  32. logical frameworks, program extraction, and other topics which give
  33. relevant background.  No prior knowledge of these topics is expected.
  34.  
  35. The systems will be demonstrated, and students will get extensive
  36. opportunities to use them in a workstation environment for developing
  37. their own proofs.
  38.  
  39. List of speakers
  40. ----------------
  41. The main speakers are
  42.  
  43.     Henk Barendregt        Jean-Louis Krivine
  44.     Stefano Berardi        Per Martin-Lof
  45.     Rod Burstall        Michel Parigot
  46.     Thierry Coquand     Christine Paulin
  47.     Gerard Huet        Randy Pollack
  48.  
  49. Location
  50. -------- 
  51. The summer school will be held in Baastad, a small town between
  52. Copenhagen and Gothenburg on the Swedish west coast.
  53.  
  54. Scholarships
  55. ------------
  56. There is a limited number of scholarships available for people who
  57. cannot obtain funding for their travel, participation fee and living
  58. expenses.  A request for full or partial support should be enclosed
  59. with the application.
  60.  
  61. Fees
  62. ----
  63. The participation fee is 4 000 SEK and room and board is 4 000 SEK.
  64.  
  65. Applications
  66. ------------
  67. Applications with a C.V. and a letter of recommendation should be sent to
  68.  
  69.         Bengt Nordstrom
  70.         - summer school -
  71.         Department of Computer Sciences
  72.         Chalmers Technical University
  73.         S - 412 96 Gothenburg, Sweden
  74.         e-mail: baastad@cs.chalmers.se
  75.  
  76. The DEADLINE for application is April 15, 1993.
  77.  
  78. Organization
  79. ------------
  80.  
  81. The school is organized by the ESPRIT Basic Research Action `Types for
  82. Proofs and Programs'. The local organization is done by Bengt
  83. Nordstrom, Peter Dybjer, Jan Smith, and Bjorn von Sydow, Gothenburg.
  84.  
  85.  
  86. -- 
  87.  
  88.     -- Lennart Augustsson
  89. [This signature is intentionally left blank.]
  90.