En el presente ejemplo vamos a escribir en **latex** la formalización del simply typed λ-calculus.  Puedes descargarte el ejemplo completo en {{:teaching:stlc.zip|}}.

Primero necesitamos listar que paquetes (packages) de latex necesitamos:

  * AmsMath.sty (incluido en texlive-2009, si no lo tiene, pueden descargar lo de: [[http://tug.ctan.org/tex-archive/macros/latex/required/amslatex/math/]])
  * Semantic.sty (incluido en texlive-2009, si no lo tiene, pueden descargar lo de: [[http://www.ctan.org/tex-archive/macros/latex/contrib/semantic/]])
  *  MathPartit.sty (no incluido en texlive-2009, deben descargar lo de: [[http://pauillac.inria.fr/~remy/latex/mathpartir.sty]], documentación en: [[http://pauillac.inria.fr/~remy/latex/mathpartir.html]])


Para nuestro ejemplo, el encabezamiento del archivo latex, debería contener:
<code latex>
\usepackage{amsmath}
\usepackage{semantic}
\usepackage{mathpartir}
</code>

Vamos a definir dos nuevos enviroments para la definición de nuestro lenguaje y para nuestras reglas de tipos y evaluación:

<code latex>
%% This new env. facilitates to write our lang. definition
\newenvironment{syntaxcategory}[1]
  {\begin{array}[l]{lcll} \multicolumn{4}{l}{\mbox{\textbf{#1}}}\\}
  {\end{array}}

%% This new env. facilitates to write our typing and evaluation rules
\newenvironment{inferbox}[0]
  {\begin{minipage}{\textwidth}\begin{mathpar}}
  {\end{mathpar}\end{minipage}}
</code>
 
Siempre es útil agregar algunos //shortcuts// para símbolos matemáticos muy usados:

<code latex>
%% Some symbol shortcuts
\mathlig{|-}{\vdash}
\mathlig{->}{\to}
\mathlig{-->}{\longrightarrow}
</code>

En el cuerpo de nuestro documento vamos agregar tres partes: (1) la definición de nuestro lenguaje (2) las reglas de derivación de tipos y por último (3) las reglas de evaluación.

====== Definición del lenguaje ======

<code latex>
\begin{displaymath}
\begin{syntaxcategory}{Language definition}
e & ::= & x \mid \lambda x \colon T. ~e \mid e ~e & \textrm{(expressions)}\\
v & ::= & \lambda x \colon T. ~e & \textrm{(values)}\\
T & ::= & T -> T  & \textrm{(types)}\\
\Gamma & ::= & \cdot \mid \Gamma[x \colon T]  & \textrm{(type env.)}\\
\end{syntaxcategory}
\end{displaymath}
</code>

====== Reglas de derivación de tipos ======

<code latex>
{\bf Typing rules} \boxed{\Gamma |- e \colon T} 

\begin{inferbox}
\inference[(t-var)]{\Gamma(x)=T} %premises
{\Gamma |- x \colon T} %conclusion
\and 
\inference[(t-abs)]{ \Gamma[x \colon T_1] |- e \colon T_2} %premises
{\Gamma |- \lambda x \colon T. ~e \colon T_1 -> T_2} %conclusion
\and
\inference[(t-abs)]{ \Gamma |- e_1 \colon T_1 -> T_2 %premise1
& \Gamma |- e_2 \colon T_1} %premise2
{\Gamma |- e_1 ~e_2 \colon T_2} %conclusion
\end{inferbox}
</code>
====== Reglas de evaluación ======

<code latex>
{\bf Evaluation rules} \boxed{e --> e'} 

\begin{inferbox}
\inference[(e-app1)]{e_1 --> e_1'} %premises
{e_1 ~e_2 --> e_1' ~e_2} %conclusion
\and 
\inference[(e-app2)]{e_2 --> e_2'} %premises
{e_1 ~e_2 --> e_1 ~e_2'} %conclusion
\and
\inference[(e-appabs)]{} 
{(\lambda x \colon T. ~e) v --> [v/x]e} %conclusion
\end{inferbox}
</code>

Al final obtenemos: {{:teaching:stlc.pdf|}}
====== Problemas conocidos ======

  * La combinación de los paquetes arriba mencionados, junto a:

<code latex>
\usepackage[spanish]{babel}
</code>

provoca resultados inesperados, i.e. algunos símbolos matemáticos (declarados como shortcuts) no son procesados.