#### Common LaTeX Commands

Here is a bare-minimum set of commands that will cover roughly 90% of your LaTeX needs, as exemplified in the following LaTeX file:

\documentclass{article} % required \usepackage{mathtools} % better support for maths \title{CS225 Spring 2018---Final Project Proposal} \author{ David Darais \\ \small{\texttt{git:@davdar}} \and Another author \\ \small{\texttt{git:@anotherauthor}} } \begin{document} \maketitle \section*{Project: System F with Existential Types} \paragraph{Extended Language} We will extend this language with the features of System F and existential types. This consists of three new types: \begin{enumerate} \item A type variable, written $X$ \item A universally quantified type, written $\forall X.\ \tau$ \item An existentially quantified type, written $\exists X.\ \tau$ \end{enumerate} The final language looks like this: \begin{equation*} \begin{array}{rcl} e & \Coloneqq & x \mid \lambda x . \ e \mid e \ e \\ & \mid & \Lambda X . e \mid e [ \tau ] \\ & \mid & \langle * e , \tau \rangle \ \texttt{as} \ \exists X . \ \tau \mid \texttt{let} \ \langle * X , x \rangle = e \ \texttt{in} \ e \end{array} \end{equation*} In ocaml the typechecker will have this type: \begin{verbatim} check : tscope * tenv * exp -> ty \end{verbatim} Note that the type environment \verb|tenv| is a mapping from \emph{variables} $x$ to types $\tau$, whereas \verb|tscope| is a set of \emph{type variables} $X$ which are in scope. \noindent If we have time, we will explore: \begin{itemize} \item $F_\omega$ \item maybe even $F_{<:}^\omega$ \end{itemize} \end{document}

Here is a minimal Makefile I like to use, which assumes your LaTeX file is named `main.tex`

:

main.pdf: main.tex mkdir -p out pdflatex --output-directory=out main.tex cp out/main.pdf ./main.pdf .PHONY: clean clean: rm -rf out rm -f main.pdf

The output of the above LaTeX file looks like this:

*Last updated April 19, 2018*