[plt-scheme] Formalizing Scheme

R5RS gives a denotational semantics for the Scheme language kernel
(http://swissnet.ai.mit.edu/~jaffer/r5rs-formal.pdf). However, its intuitive
usefulness is limited because the calculi is intricate, and the semantics is
written with a lot of abstraction (environments, stores, expconts,
cmdconts). There's nothing wrong with the semantics per se, but it doesn't
lend itself to being written down and algebraically manipulated.

The untyped lambda calculus, however, can be specified with a few axioms;
I've seen good intuitive descriptions of it in less than a page. Various
specifications of Lambda abound in many papers because it is so simple to
specify. http://citeseer.nj.nec.com/barendregt94introduction.html seems
pretty decent.

-Mike

----- Original Message -----
From: "Paulo Jorge O. C. Matos" <pocm at mega.ist.utl.pt>
To: <plt-scheme at qua.cs.brown.edu>
Sent: Monday, October 14, 2002 10:40 PM
Subject: [plt-scheme] Formalizing Scheme


>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>
> Hi all,
>
> Scheme is based in Lambda Calculus afaik. I do not know lambda calculus
> but is it possible to formalize and analyse a scheme program from a
> mathematical point of view? How? Can you please give me references?
>
> Best regards,
>
> --
> Paulo J. Matos : pocm(_at_)mega.ist.utl.pt
> Instituto Superior Tecnico - Lisbon
> Software & Computer Engineering - A.I.
>   - > http://mega.ist.utl.pt/~pocm
>   ---
> Yes, God had a deadline...
> So, He wrote it all in Lisp!
>
>