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