| A simply-typed lambda calculus |
Require Import List.
Require Import LambdaTamer.Binding.
Set Implicit Arguments.
Type language |
Syntax |
Inductive sty : Set :=
| SNat : sty
| SArrow : sty -> sty -> sty.
Denotational semantics |
Fixpoint styDenote (t : sty) : Set :=
match t with
| SNat => nat
| SArrow t1 t2 => styDenote t1 -> styDenote t2
end.
| Term language |
Syntax |
Inductive sterm : list sty -> sty -> Set :=
| SVar : forall G t,
Var G t
-> sterm G t
| SLam : forall G dom ran,
sterm (dom :: G) ran
-> sterm G (SArrow dom ran)
| SApp : forall G dom ran,
sterm G (SArrow dom ran)
-> sterm G dom
-> sterm G ran
| SConst : forall G, nat -> sterm G (SNat).
Denotational semantics |
Fixpoint stermDenote (G : list sty) (t : sty) (e : sterm G t) {struct e}
: Subst styDenote G -> styDenote t :=
match e in (sterm G t) return (Subst styDenote G -> styDenote t) with
| SVar _ _ v => VarDenote v
| SLam _ _ _ e' => fun s x => stermDenote e' (SCons _ x s)
| SApp _ _ _ e1 e2 => fun s => (stermDenote e1 s) (stermDenote e2 s)
| SConst _ n => fun _ => n
end.