\documentclass[11pt]{article} \input{defs} \setlength{\textwidth}{6in} \setlength{\oddsidemargin}{0.25in} \setlength{\evensidemargin}{0.25in} \setlength{\parskip}{5pt} \title{Typechecking Diderot} \author{ Gordon Kindlmann \\ University of Chicago \\ {\small\tt{}glk@cs.uchicago.edu} \\ \and John Reppy \\ University of Chicago \\ {\small\tt{}jhr@cs.uchicago.edu} \\ } \date{\today} \begin{document} \maketitle \thispagestyle{empty} \section{Introduction} This document looks at the rules for typechecking Diderot. \section{Types} \begin{displaymath} \begin{array}{rclr} \nu & ::= & n & \text{dimension ($n > 0$)} \\ & \mid & \phi & \text{dimension variable} \\ \sigma & ::= & \epsilon & \text{empty sequence of dimensions} \\[1em] & \mid & \rho & \text{shape variable} \\ & \mid & \sigma,\nu & \text{shape extension} \\[1em] \kappa & ::= & n & \text{$n$ levels of differentiation ($n \geq 0$)} \\ & \mid & \kappa-n & \text{} \end{array} \end{displaymath}% The syntax of Diderot types is given in \figref{fig:types}. \begin{figure}[t] \begin{displaymath} \begin{array}{rclr} \tau & ::= & \TYconst & \text{type constants} \\ & \mid & \theta \\ % & \mid & \TYmatrix{n}{m} & \text{$n\times{}m$ matrix} \\ & \mid & \TYimage{\nu}{\sigma} & \text{$d$-dimension image of $\mu$ values}\\ & \mid & \TYkern{k} & \text{convolution kernel with $k$ derivatives} \\ & \mid & \TYfield{k}{\nu}{\sigma} & \text{field} \\ \sigma & ::= \ \end{array}% \end{displaymath}% where $o\in\Nat$ is the tensor order, $d,n,m\in\SET{2,3}$ are dimensions, and $k\in\Nat$ is the differentiability of a field. \caption{Diderot types} \label{fig:types} \end{figure}% \end{document}
Click to toggle
does not end with </html> tag
does not end with </body> tag
The output has ended thus: rentiability of a field. \caption{Diderot types} \label{fig:types} \end{figure}% \end{document}