Core static semantics

doc/definition/static-semantics.tex

Index: doc/definition/static-semantics.tex
diff --git a/doc/definition/static-semantics.tex b/doc/definition/static-semantics.tex
new file mode 100644
index 0000000000000000000000000000000000000000..2b4b5be242764f2a3889c4487b7b68ac1c765e8d
--- /dev/null
+++ b/doc/definition/static-semantics.tex
@@ -0,0 +1,477 @@
+\subsection*{Expression typing: $\yieldsOk{\Phi, \Delta, \Gamma}{e}{\opt{\tau}}{e'}{\tau'}$} \hrulefill
+
+Expression typing is a relation between typing contexts, a term ($e$), an
+optional type ($\opt{\tau}$), and a type ($\tau'$).  The term $e$ represents the
+term being checked.  The optional type $\opt{\tau}$ is the type against which
+the term is being checked (if present).  The output type $\tau'$ is the most
+precise type synthesized for the term.  It should always be the case that the
+synthesized (output) type is a subtype of the checked (input) type if the latter
+is present.  The checking/synthesis pattern allows for the propogation of type
+information both downwards and upwards.  It is often the case that downwards
+propogation is not useful.  Consequently, to simplify the presentation the rules
+which do not use the checking type require that it be empty ($\_$).  The first
+typing rule allows contextual type information to be dropped so that such rules
+apply in the cast that we have contextual type information, subject to the
+contextual type being a supertype of the synthesized type:
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma} \quad\quad
+         \subtypeOf{\Phi, \Delta}{\sigma}{\tau}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau}{e'}{\sigma}} 
+
+The implicit downcast rule also allows this when the contextual type is a
+subtype of the synthesized type, corresponding to an implicit downcast.

[vsm, 2015/07/13 22:36:56]

As with the optional typing, I wonder if it's better to separate this out. 
We're currently a little inconsistent with how we handle this in the
implementation - casts to generic types are warnings, likely to fail at
runtime....

[Leaf, 2015/07/14 22:39:49]

Yes, I have mental note to revisit this.  We can have an explicit policy here
(e.g. add a premise requiring tau to be a ground type), or we can make the rules
parametric over a policy.

+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma} \quad\quad
+         \subtypeOf{\Phi, \Delta}{\tau}{\sigma}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau}{\echeck{e'}{\tau}}{\tau}} 
+
+Variables are typed according to their declarations:
+
+\axiom{\yieldsOk{\Phi, \Delta, \extends{\Gamma}{x}{\tau}}{x}{\_}{x}{\tau}}

[vsm, 2015/07/13 22:36:56]

There is type promotion - but perhaps that's orthogonal enough to ignore here.

[Leaf, 2015/07/14 22:39:49]

Yes, I could formalize this, but it will take a fair bit of machinery, and I'm
not sure it adds anything interesting.

+
+Numbers, booleans, and null all have a fixed synthesized type.
+
+\axiom{\yieldsOk{\Phi, \Delta, \Gamma}{i}{\_}{i}{\Num}}
+
+\axiom{\yieldsOk{\Phi, \Delta, \Gamma}{\eff}{\_}{\eff}{\Bool}} 
+
+\axiom{\yieldsOk{\Phi, \Delta, \Gamma}{\ett}{\_}{\ett}{\Bool}} 
+
+\axiom{\yieldsOk{\Phi, \Delta, \Gamma}{\enull}{\_}{\enull}{\Bottom}} 
+
+A $\ethis$ expression is well-typed if we are inside of a method, and $\sigma$
+is the type of the enclosing class.
+
+\infrule{\Gamma = \Gamma'_{\sigma}
+        }
+        {
+          \yieldsOk{\Phi, \Delta, \Gamma}{\ethis}{\_}{\ethis}{\sigma}
+        } 
+
+A fully annotated function is well-typed if its body is well-typed at its
+declared return type, under the assumption that the variables have their
+declared types.  
+
+\infrule{\Gamma' = \extends{\Gamma}{\many{x}}{\many{\tau}} \quad 
+         \yieldsOk{\Phi, \Delta, \Gamma'}{e}{\sigma}{e'}{\sigma'}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{\many{x:\tau}}{\sigma}{e}}
+                  {\_}
+                  {\elambda{\many{x:\tau}}{\sigma}{e'}}
+                  {\Arrow[-]{\many{\tau}}{\sigma}}

[vsm, 2015/07/13 22:36:56]

Should this be \sigma_'_?

[Leaf, 2015/07/14 22:39:50]

I think it *can* be, but not sure that it *should* be.  I think it's a bit more
standard to use the decorated type.  It's similar to the rule for local variable
bindings where we use the decorated type if given instead of using the more
precise synthesized type.  It's also a little more consistent with function
declarations this way.

+        } 
+
+A function with a missing argument type is well-typed if it is well-typed with
+the argument type replaced with $\Dynamic$.  
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\Dynamic, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\opt{\tau}}
+                  {e_f}
+                  {\tau_f}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\opt{\tau}}
+                  {e_f}
+                  {\tau_f}
+        } 
+
+A function with a missing argument type is well-typed if it is well-typed with
+the argument type replaced with the corresponding argument type from the context
+type.  Note that this rule overlaps with the previous: the formal presentation
+leaves this as a non-deterministic choice.  

[vsm, 2015/07/13 22:36:56]

Is this a step toward downward inference?

[Leaf, 2015/07/14 22:39:49]

This is downwards inference.  It's specified in a slightly odd way to keep
things readable.  Basically, these rules allow missing argument and return types
to be inferred from context. If we are in a function typed context and we are
missing an argument type, this rule allows the argument type from the context
type to be filled in. Alternatively, we can fill in the missing type with
dynamic using the other rule.  The typing rules are non-deterministic as to
which we do: the function is well-typed so long as there is *some* derivation. 
In the implementation, we will likely choose to always use the context type if
possible (that is, if the function is well-typed under that choice) in order to
minimize the number of dynamic operations.  

[vsm, 2015/07/15 18:25:34]

So, if my expr is:

(e) => e.foo

and my contextual type is:

int => int

would that type check?  The first rule appears to apply here.  Per #203, I think
we might want to disallow it.

[Leaf, 2015/07/15 22:27:25]

As currently specified, it will type check, and will reify as dynamic ->
dynamic.

The example in #203 would typecheck, but x, y, and the return type would all be
filled in with int (hence no dinvokes).

Basically, these rules allow for the contextual type to be used to fill in the
missing argument types, but don't require it (if the body can't be typed using
the more specific types, the arguments can be left as dynamic).  We could choose
to disallow the dynamic case - this would simplify the implementation in fact. 
The downside is that more programs would get rejected.

+
+\infrule{\tau_c = \Arrow[k]{\upsilon_0, \ldots, \upsilon_n}{\upsilon_r} \\
+         \yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\upsilon_i, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\tau_c}
+                  {e_f}
+                  {\tau_f}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{x_0:\opt{\tau_0}, \ldots, x_i:\_, \ldots, x_n:\opt{\tau_n}}{\opt{\sigma}}{e}}
+                  {\tau_c}
+                  {e_f}
+                  {\tau_f}
+        } 
+
+A function with a missing return type is well-typed if it is well-typed with
+the return type replaced with $\Dynamic$.  
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{\many{x:\opt{\tau}}}{\Dynamic}{e}}
+                  {\opt{\tau_c}}
+                  {e_f}
+                  {\tau_f}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{\many{x:\opt{\tau}}}{\_}{e}}
+                  {\opt{\tau_c}}
+                  {e_f}
+                  {\tau_f}
+        } 
+
+A function with a missing return type is well-typed if it is well-typed with
+the return type replaced with the corresponding return type from the context
+type.  Note that this rule overlaps with the previous: the formal presentation
+leaves this as a non-deterministic choice.  
+
+\infrule{\tau_c = \Arrow[k]{\upsilon_0, \ldots, \upsilon_n}{\upsilon_r} \\
+         \yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{\many{x:\opt{\tau}}}{\upsilon_r}{e}}
+                  {\tau_c}
+                  {e_f}
+                  {\tau_f}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\elambda{\many{x:\opt{\tau}}}{\_}{e}}
+                  {\tau_c}
+                  {e_f}
+                  {\tau_f}
+        } 
+
+
+Instance creation creates an instance of the appropriate type.
+
+% FIXME(leafp): inference
+% FIXME(leafp): deal with bounds
+\infrule{(C : \dclass{\TApp{C}{T_0,\ldots,T_n}}{\TApp{C'}{\upsilon_0, \ldots, \upsilon_k}}{\ldots}) \in \Phi \\ 
+  \mbox{len}(\many{\tau}) = n+1}
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\enew{C}{\many{\tau}}{}}
+                  {\_}
+                  {\enew{C}{\many{\tau}}{}}
+                  {\TApp{C}{\many{\tau}}}
+        } 
+
+
+Members of the set of primitive operations (left unspecified) can only be
+applied.  Applications of primitives are well-typed if the arguments are
+well-typed at the types given by the signature of the primitive.

[vsm, 2015/07/13 22:36:56]

In Dart, these are really just syntactic sugar for regular methods.  Perhaps we
don't need primitives in this subset?

Unless you want to model the weirdness around +, etc (int, int -> int and
double, double -> double per hack in spec)?

[Leaf, 2015/07/14 22:39:49]

These really model the underlying primitive operations, not the methods named
"+", etc.  In the implementations (dart2js etc) these are what are implemented
via "external" functions, or via inline JS.  These aren't very important to us
and I could leave them out, but it's a bit weird to have primitive types with no
operations on them.

+
+\infrule{\phi\, :\, \Arrow[]{\many{\tau}}{\sigma} \quad
+         \yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau}{e'}{\tau'}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\eprimapp{\phi}{\many{e}}}
+                  {\_}
+                  {\eprimapp{\phi}{\many{e'}}}
+                  {\sigma}
+        } 
+
+Function applications are well-typed if the applicand is well-typed and has
+function type, and the arguments are well-typed.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {e}
+                  {\_}
+                  {e'}
+                  {\Arrow[k]{\many{\tau_a}}{\tau_r}} \quad\quad
+         \yieldsOk{\Phi, \Delta, \Gamma}
+                  {e_a}
+                  {\tau_a}
+                  {e_a'}
+                  {\tau_a'} \quad \mbox{for}\ e_a, \tau_a \in \many{e_a}, \many{\tau_a} 
+\iftrans{\\         e_c = \begin{cases}
+                 \ecall{e'}{\many{e_a'}} & \text{if $k = -$}\\
+                 \edcall{e'}{\many{e_a'}} & \text{if $k = +$}
+                 \end{cases}}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\ecall{e}{\many{e_a}}}
+                  {\_}
+                  {e_c}
+                  {\tau_r}
+        } 
+
+Application of an expression of type $\Dynamic$ is well-typed if the arguments
+are well-typed at any type.  
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {e}
+                  {\_}
+                  {e'}
+                  {\Dynamic} \quad\quad
+         \yieldsOk{\Phi, \Delta, \Gamma}
+                  {e_a}
+                  {\_}
+                  {e_a'}
+                  {\tau_a'} \quad \mbox{for}\ e_a \in \many{e_a}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\ecall{e}{\many{e_a}}}
+                  {\_}
+                  {\edcall{e'}{\many{e_a'}}}
+                  {\Dynamic}
+        } 
+
+A dynamic call expression is well-typed so long as the applicand and the
+arguments are well-typed at any type.

[vsm, 2015/07/13 22:36:56]

What does dcall add if you allow e to be dynamic above?  The rules / operations
seem redundant.

[Leaf, 2015/07/14 22:39:49]

Basically I'm anticipating the dynamic semantics (which I haven't written in
here yet, hence the confusion).  The input program shouldn't have any
dcall/dload constructs in it (though it doesn't matter if it does).  The
elaboration rules which add in the dynamic checks turn e.m when e is dynamic
into dload(e, m), and similarly for dcall.  In the dynamic semantics, dcall and
e.m behave differently when m is not defined in e.  Basically, e.m "segfaults"
(or hard stops) and dcall throws an error (which we could choose to call no such
method).  The statement of soundness for expressions then takes the general form
that if e elaborates to E, then evaluating E will never "segfault".  That is,
what we prove is that all potentially NSM producing lookups have been translated
into dload/dcall operations which are prepared to deal with them, and all
remaining loads and calls are guaranteed to succeed.  This notion of soundness
is what validates the compilation of Dart field load/method call directly into
JS property load.

[Siggi Cherem (dart-lang), 2015/07/14 23:59:21]

Makes sense - I think it might be worth splitting the input language from the
output of the translation in the future. Maybe even include a different term for
the segfault cases (scall/sload) to avoid confusing input-language terms with
the translated language terms.

[vsm, 2015/07/15 18:25:34]

It's the same thing (I think), but it might be a little clearer to think about
if you expressed this as e(x) is typed if e is dynamic and dcall(e, x) is typed.

 

[Leaf, 2015/07/15 22:27:25]

Yes, this is reasonable.  I need additional mechanism for the dynamic semantics
anyway.  I'll either split out these terms, or mark them in some way as just
part of the translation/dynamic semantics.

[Leaf, 2015/07/15 22:27:25]

Done.

+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {e}
+                  {\_}
+                  {e'}
+                  {\tau} \quad
+         \yieldsOk{\Phi, \Delta, \Gamma}
+                  {e_a}
+                  {\_}
+                  {e_a'}
+                  {\tau_a} \quad \mbox{for}\ e_a \in \many{e_a}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\edcall{e}{\many{e_a}}}
+                  {\_}
+                  {\edcall{e'}{\many{e_a'}}}
+                  {\Dynamic}
+        }
+
+A field load is well-typed if the term is well-typed, and the field name is
+present in the type of the term.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {e}
+                  {\_}
+                  {e'}
+                  {\sigma} \quad\quad
+         \fieldLookup{\Phi}{\sigma}{m}{\tau}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\eload{e}{m}}
+                  {\_}
+                  {\eload{e'}{m}}
+                  {\tau}
+        }
+
+A field load from a term of type $\Dynamic$ is well-typed if the term is
+well-typed.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {e}
+                  {\_}
+                  {e'}
+                  {\Dynamic} 
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\eload{e}{m}}
+                  {\_}
+                  {\edload{e'}{m}}
+                  {\Dynamic}
+        }
+
+A dynamic load is well typed so long as the term is well-typed.

[vsm, 2015/07/13 22:36:56]

Ditto?

+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {e}
+                  {\_}
+                  {e'}
+                  {\Dynamic} 
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\edload{e}{m}}
+                  {\_}
+                  {\edload{e'}{m}}
+                  {\Dynamic}
+        }
+
+An assignment expression is well-typed so long as the term is well-typed at a
+type which is compatible with the type of the variable being assigned.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {e}
+                  {\opt{\tau}}
+                  {e'}
+                  {\sigma} \quad
+        \yieldsOk{\Phi, \Delta, \Gamma}
+                  {x}
+                  {\sigma}
+                  {x}
+                  {\sigma'}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\eassign{x}{e}}
+                  {\opt{\tau}}
+                  {\eassign{x}{e'}}
+                  {\sigma}
+        } 

[vsm, 2015/07/13 22:36:56]

This reads a little odd to me ... seems to suggest that the synthesized type of
e must exactly match the declared type of x.  I would expect subtyping or
assignability here.

[Leaf, 2015/07/14 22:39:49]

The way it works here is a bit subtle, but I think it all works out.  Remember
that the rule is that if e checks at \opt{\tau} and synthesizes to \sigma, then
\tau (if present) is a super type of \sigma.  That is, the synthesized type is a
subtype of the checked (context) type.  So here, checking e checks that it is
well-typed at \tau, and has some type \sigma which is a subtype of \tau.  Then
we check that x checks at \sigma and synthesizes to some \sigma' (and hence that
\sigma' is a subtype of \sigma).  Concretely, the variable rule does not apply
when the checked type (\sigma) is not \_, so we apply the subsumption rule which
says that x is well-typed as \sigma if x is well-typed at \_ and synthesizes to
some \sigma' which is a subtype of \sigma.    A variable x synthesizes to
\sigma' if that is its declared type, so we end up checking exactly what you
expect: that the type of e is a subtype of the declared type of e.  If we wanted
to loosen this to some kind of assignability, we could add some additional
mechanism here.  Note that the downcast rule can be applied instead of the
subsumption rule here already though, so the assignment will still be valid if
\sigma is a subtype of \sigma'.  There will just be cast added during
elaboration.

In the implementation of course the uses of the subsumption and downcast rules
get folded into the other rules via checkAssignment.  This avoids the
non-deterministic choice as to when to apply subsumption.  But for the purposes
of the specification, this simplifies the other rules substantially.

+
+A field assignment is well-typed if the term being assigned is well-typed, the
+field name is present in the type of $\ethis$, and the declared type of the
+field is compatible with the type of the expression being assigned.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {e}
+                  {\opt{\tau}}
+                  {e'}
+                  {\sigma} \quad\quad
+        \Gamma = \Gamma_\tau & \fieldLookup{\Phi}{\tau}{m}{\sigma'} \quad
+        \subtypeOf{\Phi, \Delta}{\sigma}{\sigma'}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\eset{\ethis}{m}{e}}
+                  {\opt{\tau}}
+                  {\eset{\ethis}{m}{e}}
+                  {\sigma}
+        } 
+
+A throw expression is well-typed at any type.
+
+\axiom{\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\ethrow}
+                  {\_}
+                  {\ethrow}
+                  {\sigma}
+        } 
+
+A cast expression is well-typed so long as the term being cast is well-typed.
+The synthesized type is the cast-to type.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\eas{e}{\tau}}
+                  {\_}
+                  {\eas{e'}{\tau}}
+                  {\tau}
+        } 
+
+An instance check expression is well-typed if the term being checked is
+well-typed.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\eis{e}{\tau}}
+                  {\_}
+                  {\eis{e'}{\tau}}
+                  {\Bool}
+        } 

[vsm, 2015/07/13 22:36:56]

Should \tau be required to be ground here and above?

[Leaf, 2015/07/14 22:39:49]

Yes.

[Leaf, 2015/07/14 22:39:49]

Done.

+
+A check expression is well-typed so long as the term being checked is
+well-typed.  The synthesized type is the target type of the check.
+
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\sigma}
+        }
+        {\yieldsOk{\Phi, \Delta, \Gamma}
+                  {\echeck{e}{\tau}}
+                  {\_}
+                  {\echeck{e'}{\tau}}
+                  {\tau}
+        } 
+
+\subsection*{Declaration typing: $\declOk[d]{\Phi, \Delta, \Gamma}{\mathit{vd}}{\mathit{vd'}}{\Gamma'}$}
+\hrulefill
+
+Variable declaration typing checks the well-formedness of the components, and
+produces an output context $\Gamma'$ which contains the binding introduced by
+the declaration.
+
+A simple variable declaration with a declared type is well-typed if the
+initializer for the declaration is well-typed at the declared type.  The output
+context binds the variable at the declared type.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau}{e'}{\tau'} \quad 
+        }
+        {\declOk[d]{\Phi, \Delta, \Gamma}
+                {\dvar{x:\tau}{e}}
+                {\dvar{x:\tau'}{e'}}
+                {\extends{\Gamma}{x}{\tau}}
+        }
+
+A simple variable declaration without a declared type is well-typed if the
+initializer for the declaration is well-typed at any type.  The output context
+binds the variable at the synthesized type (a simple form of type inference).
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\tau'} \quad 
+        }
+        {\declOk[d]{\Phi, \Delta, \Gamma}
+                {\dvar{x:\_}{e}}
+                {\dvar{x:\tau'}{e'}}
+                {\extends{\Gamma}{x}{\tau'}}
+        }
+
+A function declaration is well-typed if the body of the function is well-typed
+with the given return type, under the assumption that the function and its
+parameters have their declared types.  The function is assumed to have a
+contravariant (precise) function type.  The output context binds the function
+variable only.
+
+\infrule{\tau_f = \Arrow[-]{\many{\tau_a}}{\tau_r} \quad 
+         \Gamma' = \extends{\Gamma}{f}{\tau_f} \quad
+         \Gamma'' = \extends{\Gamma'}{\many{x}}{\many{\tau_a}} \\
+         \stmtOk{\Phi, \Delta, \Gamma''}{s}{\tau_r}{s'}{\Gamma_0}
+        }
+        {\declOk[d]{\Phi, \Delta, \Gamma}
+                {\dfun{\tau_r}{f}{\many{x:\tau_a}}{s}}
+                {\dfun{\tau_r}{f}{\many{x:\tau_a}}{s'}}
+                {\Gamma'}
+        }
+
+\subsection*{Statement typing: $\stmtOk{\Phi, \Delta, \Gamma}{\mathit{s}}{\tau}{\mathit{s'}}{\Gamma'}$}
+\hrulefill
+
+The statement typing relation checks the well-formedness of statements and
+produces an output context which reflects any additional variable bindings
+introduced into scope by the statements.
+
+A variable declaration statement is well-typed if the variable declaration is
+well-typed per the previous relation, with the corresponding output context.
+
+\infrule{\declOk[d]{\Phi, \Delta, \Gamma}
+                {\mathit{vd}}
+                {\mathit{vd'}}
+                {\Gamma'}
+        }
+        {\stmtOk{\Phi, \Delta, \Gamma}
+                {\mathit{vd}}
+                {\tau}
+                {\mathit{vd'}}
+                {\Gamma'}
+        }
+
+An expression statement is well-typed if the expression is well-typed at any
+type per the expression typing relation. 
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\_}{e'}{\tau}
+        }
+        {\stmtOk{\Phi, \Delta, \Gamma}{e}{\tau}{e'}{\Gamma}
+        }
+
+A conditional statement is well-typed if the condition is well-typed as a
+boolean, and the statements making up the two arms are well-typed.  The output
+context is unchanged.
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\Bool}{e'}{\sigma} \quad
+         \stmtOk{\Phi, \Delta, \Gamma}{s_1}{\tau_r}{s_1'}{\Gamma_1} \quad
+         \stmtOk{\Phi, \Delta, \Gamma}{s_2}{\tau_r}{s_2'}{\Gamma_2} 
+        }
+        {\stmtOk{\Phi, \Delta, \Gamma}
+                {\sifthenelse{e}{s_1}{s_2}}
+                {\tau_r}
+                {\sifthenelse{e'}{s_1'}{s_2'}}
+                {\Gamma}
+        }
+
+A return statement is well-typed if the expression being returned is well-typed
+at the given return type.  
+
+\infrule{\yieldsOk{\Phi, \Delta, \Gamma}{e}{\tau_r}{e'}{\tau}
+        }
+        {\stmtOk{\Phi, \Delta, \Gamma}{\sreturn{e}}{\tau_r}{\sreturn{e'}}{\Gamma}
+        }
+
+A sequence statement is well-typed if the first component is well-typed, and the
+second component is well-typed with the output context of the first component as
+its input context.  The final output context is the output context of the second
+component.
+
+\infrule{\stmtOk{\Phi, \Delta, \Gamma}{s_1}{\tau_r}{s_1'}{\Gamma'} \quad
+         \stmtOk{\Phi, \Delta, \Gamma'}{s_2}{\tau_r}{s_2'}{\Gamma''}
+        }
+        {\stmtOk{\Phi, \Delta, \Gamma}{s_1;s_2}{\tau_r}{s_1';s_2'}{\Gamma''}
+        }