\documentclass{letter}
\usepackage{mathpazo}
\usepackage{url}
\usepackage{hyperref}
\usepackage{breakurl}

\usepackage[official]{eurosym}
%\usepackage[scaled=.84]{beramono}

\newcommand\tlaplus{TLA\smash{\kern-.1ex\textsuperscript{+}}}
\newcommand\tlaps{\tlaplus{} Proof System}

\newcommand\httpx[2]{\href{http:#1}{#2}}
\newcommand\http[1]{\httpx{#1}{\nolinkurl{#1}}}
\newcommand\email[1]{\href{mailto:#1}{\nolinkurl{#1}}}
\newcommand\const[1]{\textsf{#1}}
\newcommand\keyw[1]{\textbf{#1}}

\newcommand\cpp{C\raise.1ex\hbox{+}\raise.1ex\hbox{+}}

\hyphenation{data-type data-types co-data-type co-data-types Isa-belle}

\begin{document}

\thispagestyle{empty}

\centerline{\large \bfseries Arithmetic and casting in Lean}

\medskip
%\vskip1.5\smallskipamount

\begin{description}
\item[Topic:] Logic, Verification
\item[Location:] Vrije Universiteit Amsterdam, The Netherlands
\item[Supervisors:] ~\\[\jot] 
  Dr.\ Robert Y. Lewis (\email{r.y.lewis@vu.nl}) \\
  Dr.\ Jasmin Christian Blanchette (\email{j.c.blanchette@vu.nl})

%\item[Senior Researchers:] ~\\
%Dr.\ Stephan Merz (\email{stephan.merz@loria.fr}, Inria) \\
%Dr.\ Christoph Weidenbach (\email{weidenbach@mpi-inf.mpg.de}, MPI)
\item[Background:] ~\\[\jot]
\textbf{Proof assistants} (also called interactive theorem provers) make it
possible to develop computer-checked, formal proofs of theorems. The primary
advantage of formal proofs is the extremely high trustworthiness of the result.
%
Proof assistants are employed for hardware and software verification at AMD and
Intel. Two recent groundbreaking applications are a verified C compiler and a
verified operating system microkernel.

\vskip1.5\smallskipamount

\textbf{Lean} [1] is a disruptive proof assistant developed at Microsoft
Research and Carnegie Mellon University.
Lean draws on decades of experience in interactive and automatic theorem
provers (e.g., Coq, Isabelle/HOL, and Z3).
It is
based on type theory, a highly expressive logic with a very rich dependent type system
(similar to Coq's) that can capture correctness properties of programs (e.g., ``the \texttt{quicksort}
function returns a sorted list''). It is implemented in \cpp{}.

%is a new system based
%on similar ideas but takes a fresh look at many of Coq's design decisions. It
%puts the emphasis on efficiency, trustworthiness, and automatic proof
%generation, and has the potential to become a serious competitor to Coq.
%It is implemented in \cpp{}.

\vskip1.5\smallskipamount

\item[Objective:] ~\\[\jot]
Constructing formal proofs by hand can be tedious, especially when dealing with simple numeric or arithmetic facts. We often want the system to manage such proofs for us. Another related problem involves moving between related or embedded types, for example from $\mathbb{N}$ to $\mathbb{Z}$ to $\mathbb{Q}$. Many facts are preserved when we embed terms of one type into another type, but the embeddings can confuse automated tools and frustrate users.

\vskip1.5\smallskipamount

Various proof assistants have tools and idioms for handling both of these tasks. Decision procedures for linear arithmetic are well known in the literature and can be implemented in proof-producing ways [2]. Lean has some support for continuous (rational) arithmetic; the problem for discrete (integer) arithmetic is harder, as is supporting quantifiers. Processes for manipulating casts can be incorporated into simplifiers or implemented independently.

\vskip1.5\smallskipamount

\textbf{The goal of this project is to adapt such tools for integer arithmetic and casting to Lean.} This can be approached from many different directions. One is to design a \emph{simplifier loop}, a tool that generalizes Lean's simplifier to incorporate simplifier procedures (\emph{simprocs}). Both arithmetic and cast management can be implemented in this framework. The tools can also be approached independently, e.g. integer arithmetic can be designed as an extension of the current rational arithmetic or in a novel way.

\vskip1.5\smallskipamount

Lean features a powerful \emph{metaprogramming} framework that is used to write proof-producing automation using the language of Lean itself. The tools described here will be implemented in this language.

\vskip1.5\smallskipamount

This internship is an ideal opportunity to familiarize oneself with proof
assistants and to get acquainted with the exciting research taking place at
the \textbf{Vrije Universiteit Amsterdam}.
This work will likely be part of a publication at an international
conference (e.g., \emph{Certified Programs and Proofs} or \emph{Interactive
Theorem Proving}).

\item[Requirements:] ~\\[\jot]
We expect the student to be familiar with the $\lambda$-calculus and both
imperative (e.g., C/\cpp) and functional programming (e.g., Haskell or OCaml)
and to have a basic understanding of logic. We do \emph{not} expect
familiarity with a proof assistant. Knowledge of Dutch is not required.

\item[Compensation:] ~\\[\jot]
In addition to any compensation offered by the intern's home institution, we offer \euro{250} per month and will reimburse travel expenses to Amsterdam.

\item[References:] % ~\\[0pt]
\end{description}

\kern-3.5\smallskipamount

\begin{raggedright}
\begin{itemize}
\item[{[1]}] Leonardo de Moura,
               Soonho Kong,
               Jeremy Avigad,
               Floris van Doorn, and
               Jakob von Raumer. \emph{The Lean Theorem Prover (System Description).}
  CADE 2015, pp.~378--388.
  
\item[{[2]}] Fr\'ed\'eric Besson. \emph{Fast Reflexive Arithmetic Tactics: The Linear Case and Beyond.} TYPES 2006, pp.~48--62.

\item[{[3]}] Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura. \emph{A Metaprogramming Framework for Formal Verification.} ICFP 2017, pp.~1--29.

\end{itemize}
\end{raggedright}

\end{document}
