The Coq mailing list

[Nick Benton <nick AT microsoft.com>]

Hi Norman,

A reasonably short (320 lines or so, for what that's worth) development of 
STLC using strongly typed syntax, including operational and denotational 
semantics and an adequacy proof relating them, is described here: 
http://research.microsoft.com/en-us/um/people/nick/jartypedsyntax.pdf
with the scripts here: 
http://research.microsoft.com/en-us/um/people/nick/jartypedsyntaxcoq.zip

That doesn't entirely meet your criteria, as it combines term syntax and 
typing, but it does include the denotational model you were looking for.

 Nick

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Frederic Blanqui
Sent: 15 November 2012 13:49
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] STLC development

Hello Norman.

You can find a formalization of 1-6 in http://color.inria.fr/ using named 
variables (no de Bruijn indices) and explicit alpha-equivalence.

Le 15/11/2012 09:51, Norman Danner a écrit :
> Hello list,
>
> I am looking for a development of the simply-typed lambda calculus 
> that I could look at, as I'm having some trouble doing this on my own.  
> I suspect my difficulties are not deep.  What I'm looking for is a 
> development along the following lines:
>
> 1. A definition of expressions (nothing complicated; just variables,
>     natural number constants, abstraction, and application).

The definition of terms is parameterized by a set of constants (you can take 
nat for it if you want). See 
http://color.inria.fr/doc/CoLoR.Term.Lambda.LTerm.html for the definitions 
and lemmas.

> 2. A definition of type (nothing complicated; just N and arrow types).
> 3. A notion of type context.
> 4. A definition of 'typed G t tau', where Pi : typed G t tau means that
>     Pi is a derivation that t has type tau under type context G (below,
>     G |- t : tau).

See http://color.inria.fr/doc/CoLoR.Term.Lambda.LSimple.html .

> 5. A notion of substitution on expressions.

See http://color.inria.fr/doc/CoLoR.Term.Lambda.LSubs.html .

> 6. A proof that if G, x : sigma |- t : tau and G |- s : sigma, then
>     G |- t[s/x] : tau.

See lemma tr_subs in
http://color.inria.fr/doc/CoLoR.Term.Lambda.LSimple.html .

> 7. The standard full-function-space denotational semantics using nat
>     and -> to interpret N and arrow types, where den Pi xi is the
>     denotation of (the typing of) the expression t under environment
>     xi (i.e., really a definition of
>     den {G} {t} {tau} (Pi : typed G t tau) xi).

By "full-function-space", do you mean the set-theoretical function space
F(A,B) that includes non-computable functions too? If so, the Coq space 
A->B is not enough.

Frederic.

> 8. A proof that if Pi is a derivation of G |- t[s/x] : tau obtained
>     from derivations Pi_t of G, x:sigma |- t:tau and
>     Pi_s of G |- s:sigma, then
>     den Pi xi = den Pi_t (xi[x |-> den Pi_s xi]).
>
> I can do 1-7 without much difficulty.  8 is killing me.  I assume it is
> because I am doing something sub-optimally somewhere in 1-7.
>
> I'm sure I'm not the first person to try to do this, and I think the
> most efficient way to solve my difficulties is to see it done right.  I
> would be grateful for pointers to solutions.  Thanks!
>
>      - Norman
>