SH@XX.LCS.MIT.EDU.UUCP (05/09/86)
Friday, May 9, l986 TALK 1: 10:00 a.m., TALK 2: 2:00 p.m. 2nd Floor Lounge David Turner University of Kent at Canterbury, England TALK 1: Intuitionist Logic and Functional Programming Intuitionism is a heretical school of mathematics founded by L. E. J. Brouwer in l907. The most outstanding characteristic of intuitionists is that they reject the use of Boolean logic. Recent discoveries have shown that there is deep underlying connection between intuitionist logic and functional programming. This discovery is likely to have profound consequences for the future of both subjects. The talk will attempt to explain from the beginning what intuitionist logic is about and how the coincidence with functional programming arises. TALK 2: Constructive Type Theory as a Programming Language Constructive type theory is a formal logic and set theory which has been developed by Per Martin-Lof as a foundation for constructive (or intuitionist) mathematics. Curiously, it can also be read as a (strongly typed) functional programming language, with a number of unusual properties, including that all well typed programs terminate. The talk will give an overview of the main ideas in constructive type theory from the point of view of someone trying to use it as a programming language. HOST: Professors Arvind and Rishiyur S. Nikhil