Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!allegra!princeton!caip!lll-crg!mordor!styx!XX.LCS.MIT.EDU!LISA
From: LISA@XX.LCS.MIT.EDU (Lisa F. Melcher)
Newsgroups: mod.ai
Subject: Seminar - Dependent Types (MIT)
Message-ID: <12213756018.29.LISA@XX.LCS.MIT.EDU>
Date: Tue, 10-Jun-86 14:45:38 EDT
Article-I.D.: XX.12213756018.29.LISA
Posted: Tue Jun 10 14:45:38 1986
Date-Received: Wed, 18-Jun-86 03:12:13 EDT
Sender: daemon@styx.UUCP
Organization: The ARPA Internet
Lines: 26
Approved: ailist@sri-ai.arpa


                        Date:  Thursday, June 19, 1986
                        Time:  2:45 p.m......Refreshments
                               3:00 p.m......Lecture
                       Place:  NE43 - 512A



                  "DEPENDENT TYPES -- FIFTEEN YEARS LATER"


                                 J.Y.GIRARD
                           University of Paris VII


Our system F of polymorphic lambda calculus (developed independently by
Reynolds) is attracting increasing interest because of its relation to
polymorphic types in programming, although our original motivation for
studying the system was quite different.  In this talk we summarize the basic
theoretical properties of the type system and compare the computer
scientists' and logicians' views of it. 



              Sponsored by TOC, Laboratory for Computer Science
                             Albert Meyer, Host