Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] View of /papers/modulespaper/design/figs/fig-statsem.tex
ViewVC logotype

View of /papers/modulespaper/design/figs/fig-statsem.tex

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3564 - (download) (as text) (annotate)
Thu Sep 30 13:33:05 2010 UTC (8 years, 10 months ago) by dbm
File size: 1189 byte(s)
initial import
%!TEX root = ../principles.tex
\begin{figure}
\centering
\fixedCodeFrame{
\small
\[
\setlength{\tabcolsep}{0ex}
\renewcommand{\arraystretch}{1.1}
\begin{array}{ll}
	\infer[\rlabel{local}]{\begin{array}{l}\Gamma\vdash\local~\overline{d_1}~\inx~\overline{d_2}~\en\\
	\Rightarrow(\underline{\local}~\underline{\overline{d_1}}~\inx~\underline{\overline{d_2}}~\en,entdec,\Gamma_2,\Delta)\end{array}}
		{\Gamma\vdash\overline{d_1}\Rightarrow(\underline{\overline{d_1}},entdec_1,\Gamma_1,\Delta_1)\\ 
 \Gamma\oplus\Gamma_1\vdash\overline{d_2}\Rightarrow(\underline{\overline{d_2}},entdec_2,\Gamma_2,\Delta_2)}
\\
\qquad
\\
\infer[\rlabel{type}]{\Gamma\vdash\type~\overline{\alpha}~t=\tau\Rightarrow(,entdec,\Gamma,\Delta)}
{\strut}
\\
\qquad
\\
\infer[\rlabel{sig}]{\Gamma\vdash\sig{\overline{spec}}\Rightarrow(\sig{\overline{spec}},\bullet,\Gamma',\emptyset)}{\strut}
\\
\qquad
\\
\infer[\rlabel{structure}]{\Gamma\vdash\struct{\overline{ld}}\Rightarrow\struct{\overline{ld}}}{}
\end{array}
\]
}
The underline notation denotes the elaborated version of the nonterminal, i.e., the explicitly typed and elaborated variant.
\nocaptionrule
\caption{Static Semantics}
\label{fig:statsem}
\end{figure}

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0