Subject: Re: Constructive mathematics
From: Matthias Felleisen (firstname.lastname@example.org)
Date: Wed Jan 30 2002 - 21:39:54 EST
To be precise, the type system of a simply typed lambda calculus
corresponds to intuitionistic logic. The arrow is intuitionistic
implication. There is no law of the excluded middle, etc.
A proof in IL corresponds to a type and with it a program in SLC.
We will discuss this a bit on Monday.
IL isn't quite constructivism, though it is close.
You need to understand that there is no such thing as "the" logic. Each
approach to logic has its place somewhere in CS.
This archive was generated by hypermail 2b28 : Wed Jan 30 2002 - 21:40:00 EST