**Subject: **Re: Constructive mathematics

**From: **Matthias Felleisen (*matthias@ccs.neu.edu*)

**Date: **Wed Jan 30 2002 - 21:39:54 EST

**Reply****Next message:**Matthias Felleisen: "homework"**Previous message:**Philippe Meunier: "deBruijn vs alpha-renaming"**In reply to:**Macneil Shonle: "Constructive mathematics"**Reply:**Matthias Felleisen: "Re: Constructive mathematics"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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.

-- Matthias

**Next message:**Matthias Felleisen: "homework"**Previous message:**Philippe Meunier: "deBruijn vs alpha-renaming"**In reply to:**Macneil Shonle: "Constructive mathematics"**Reply:**Matthias Felleisen: "Re: Constructive mathematics"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

*
This archive was generated by hypermail 2b28
: Wed Jan 30 2002 - 21:40:00 EST
*