Another introduction, with emphasis on the historical development:
Philip Wadler, "Proofs are Programs: 19th Century Logic and 21st
Century Computing."
http://www.cs.bell-labs.com/who/wadler/topics/history.html
It's a fun read, too.
Cheers,
Tom
_
> and not just type systems but also other aspects of operational
> semantics. What we have here is a single rule from a rule-based
> inductive definition of a certain relation G |- s :: S between typing
> environments G, expressions s and types S.
It's probably worth mentioning here that this n
Juan Carlos Arevalo Baeza wrote (on 28-05-01 18:02 -0700):
>
> Just a very naive question, because I'm really curious. I've seen in
> previous messages here discussions about type systems using this kind of
> notation:
>
> > G |- f :: all x::S . T G |- s :: S
> >
> > > G |- f :: all x::S . T G |- s :: S
> > >--
> > > G |- f s :: [s/x]T
>
Any more takers? I still don't have any pointers to literature where
this theorem notation is explained more fully, and
- Original Message -
From: "Juan Carlos Arevalo Baeza" <[EMAIL PROTECTED]>
To: <[EMAIL PROTECTED]>
Sent: Tuesday, May 29, 2001 11:02 AM
Subject: Notation question
>
> Just a very naive question, because I'm really curious. I've seen in
> prev
At 09:24 PM 5/28/2001 -0400, Mark Carroll wrote:
> > > G |- f :: all x::S . T G |- s :: S
> > >--
> > > G |- f s :: [s/x]T
>
>I'm far from the right person to have a go, but while we're waiting for
>someone who knows what they're talking about:
On Mon, 28 May 2001, Juan Carlos Arevalo Baeza wrote:
>
> Just a very naive question, because I'm really curious. I've seen in
> previous messages here discussions about type systems using this kind of
> notation:
>
> > G |- f :: all x::S . T G |- s :: S
> >
Just a very naive question, because I'm really curious. I've seen in
previous messages here discussions about type systems using this kind of
notation:
> G |- f :: all x::S . T G |- s :: S
>--
> G |- f s :: [s/x]T
I'd never seen it befor
