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}
  David Darais \\ \small{\texttt{git:@davdar}}
  Another author \\ \small{\texttt{git:@anotherauthor}}


\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:
\item A type variable, written $X$
\item A universally quantified type, written $\forall X.\ \tau$
\item An existentially quantified type, written $\exists X.\ \tau$
The final language looks like this:
    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
                    \texttt{let} \ \langle * X , x \rangle = e \ \texttt{in} \ e
In ocaml the typechecker will have this type:
check : tscope * tenv * exp -> ty
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.

If we have time, we will explore:
\item $F_\omega$
\item maybe even $F_{<:}^\omega$


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
	rm -rf out
	rm -f main.pdf

The output of the above LaTeX file looks like this:

latex output image

Last updated April 19, 2018