[mod.ai] Seminar - Intuitionist Logic & Constructive Type Theory

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