working on intro

axioms.tex

@@ -208,7 +208,7 @@ \subsubsection{The computation rule ($\iota$ reduction)}\label{sec:iota}
 This rule suffices for the theoretical presentation, but there is a second reduction rule called ``K-like reduction'' used for subsingleton eliminators. It can be thought of as a combination of proof irrelevance to change the major premise into a constructor followed by the iota rule.
 
 $$\frac{F=\forall a::\alpha.\;\P}{\rec_P\;C\;e\;p[b]\;h\rightsquigarrow e_c\;b\;v}$$
-This rule only applies when all the variables in $b$ are actually on the LHS, which is the reason for the peculiar requirements on subsingleton eliminators. If $b_i$ appears in the parameters for its type, that means that $p_j[b]=b_i$ for some $j$, and so $b_i$ is on the LHS. 
+This rule only applies when all the variables in $b$ are actually on the LHS, which is the reason for the peculiar requirements on subsingleton eliminators. If $b_i$ appears in the parameters for its type, that means that $p_j[b]=b_i$ for some $j$, and so $b_i$ is on the LHS.
 
 The foremost example of this is known in the literature as axiom K, which is the reason for the name ``K-like reduction'', which is this principle applied to the equality type:
 $$\mathsf{rec}_{a=}\;C\;x\;a\;h\equiv x$$
@@ -242,3 +242,5 @@ \subsubsection{Axiom of choice}
 \mathsf{choice}&:\forall\alpha:\U_u.\;\nonempty\;\alpha\to\alpha
 \end{align*}
 From the axiom of choice, the law of excluded middle is derived (it is not stated as a separate axiom).
+
+\subsection{Differences from \textsf{Coq}}\label{sec:notcoq}

intro.tex

@@ -1,7 +1,24 @@
 \section{Introduction}
-In this paper, we develop the foundational theory used in the Lean theorem prover.
+\subsection{Type theory in programming languages}
+The history of types in mathematical logic dates back to Frege's \emph{Begriffsschrift} \cite{frege}, which establishes a notation system for what amounts to second-order logic with equality. Bertrand Russell discovered a paradox in Frege's system: The predicate $P(A):=\neg A(A)$ leads to a contradiction (or in set-theoretic notation, the set $S=\{x\mid x\notin x\}$ cannot be a set). In reaction, Ernst Zermelo resolved the contradiction by imposing a ``size restriction'' on sets, leading to Zermelo set theory and eventually to Zermelo-Fraenkel set theory (ZFC), which has become the gold standard for axiomatization in modern mathematics. This yields an untyped but stratified view of the universe of mathematical concepts.
 
+Russell's own reaction to Russell's paradox was instead to impose a stratification on the language itself, rejecting the expressions $A(A)$ or $x\in x$ as ``ill-typed''. This line of reasoning says that $A$ is not an object that predicates on objects of the same type as itself, so the notion is prima facie ill-formed. This idea is developed in \emph{Principia Mathematica} \cite{principia} and Quine's New Foundations \cite{quinenf}, but the most relevant application was to the simply typed $\lambda$-calculus \cite{churchstt} by Church (1940).
+
+Somewhat independently, programming languages rediscovered the idea of a type \cite{typesoftypes}. Early programming languages had no explicit notion of type. Lisp used an evaluation model closely related to the untyped $\lambda$-calculus. FORTRAN (1956) had ``modes'' of expressions, either fixed or floating point. Algol 60 (1960) developed expressions and variables of type (\textbf{integer}, \textbf{real}, \textbf{Boolean}), and the extension Algol W by Wirth and Hoare (1966) developed a generative syntax for types including record types and typed references.
+
+The logical and programming traditions are finally explicitly connected in the Curry-Howard isomorphism \cite{curryhoward}, which observed the connection between logical derivations (in the sequent calculus) and lambda terms in the simply typed $\lambda$-calculus. (In the same correspondence, Howard also discusses extensions to first order logic, with lambdas ranging over ``number variables'' $(\lambda x.\,F^\beta)^{\forall x\,\beta}$ separate from typed lambdas $(\lambda X^\alpha.\,F^\beta)^{\alpha\supset\beta}$.) But dependent type theory really begins in earnest with Per Martin-L\"{o}f \cite{martinlof}, who set the foundations for Brouwer's intuitionistic type theory as an outgrowth of the simply typed $\lambda$-calculus with dependent types.
+
+Martin-L\"{o}f describes how constructive type theory can be used in programming languages:
+\begin{quote}
+By choosing to program in a formal language for constructive mathematics, like the theory of types, one gets access to the whole conceptual apparatus of pure mathematics, neglecting those parts that depend critically on the law of excluded middle, whereas even the best high level programming languages so far designed are wholly inadequate as mathematical languages (and, of course, nobody has claimed them to be so). In fact, I do not think that the search for logically ever more satisfactory high level programming languages can stop short of anything but a language in which (constructive) mathematics can be adequately expressed. \cite{martinlofprog}
+\end{quote}
+
+This dream was converted to action by Thierry Coquand, who developed the Calculus of Constructions (CoC) \cite{coquandcoc} and developed an interactive proof assistant \textsf{Coq} to check proofs in this language \cite{coqart}. This type theory was extended with inductive types \cite{dybjer} to form the Calculus of Inductive Constructions (CIC) \cite{paulincic}.
+
+Lean \cite{demoura} is a theorem prover based on CIC as well, with some subtle but important differences. See \autoref{sec:notcoq} for an elaboration of the differences from Coq's axiomatics. The goal of this paper is to demonstrate the consequences of these differences, without leaving anything out. While CIC itself is well-studied \cite{barrassets, barrastypedec, coqincoq}, most papers study subsystems of the actual axiomatic system implemented in Coq, which might be called $\mathsf{CIC^+}$ for its many small extensions added over the years. While we will not analyze $\mathsf{CIC^+}$ in this paper, we will be able to analyze all the extensions that are in Lean CIC, so our proof of consistency is directly applicable to the full Lean kernel.
+
+UNFINISHED: talk about:
 \begin{itemize}
 \item Werner \cite{setsintypes}: Sets in Types
-\item Miquel \cite{notsosimple}: The not so simple CC
+\item Miquel \cite{notsosimple}: The not so simple proof irrelevant model of CC
 \end{itemize}

main.tex

@@ -110,6 +110,7 @@
 \input{abstract}
 \tableofcontents  % Print table of contents
 
+\pagebreak
 \input{intro}
 \input{axioms}
 \input{typesys}

references.bib

@@ -28,3 +28,132 @@ @inproceedings{ecc
   year={1989},
   organization={IEEE}
 }
+@inproceedings{typesoftypes,
+  title={Several types of types in programming languages},
+  author={Martini, Simone},
+  booktitle={International Conference on History and Philosophy of Computing},
+  pages={216--227},
+  year={2015},
+  organization={Springer}
+}
+@article{frege,
+  title={Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought},
+  author={Frege, Gottlob},
+  journal={From Frege to G{\"o}del: A source book in mathematical logic},
+  volume={1931},
+  pages={1--82},
+  year={1879}
+}
+@book{principia,
+  title={Principia mathematica},
+  author={Whitehead, Alfred North and Russell, Bertrand},
+  volume={2},
+  year={1912},
+  publisher={University Press}
+}
+@article{quinenf,
+  title={New foundations for mathematical logic},
+  author={Quine, Willard V},
+  journal={The American mathematical monthly},
+  volume={44},
+  number={2},
+  pages={70--80},
+  year={1937},
+  publisher={Taylor \& Francis}
+}
+@article{churchstt,
+  title={A formulation of the simple theory of types},
+  author={Church, Alonzo},
+  journal={The journal of symbolic logic},
+  volume={5},
+  number={2},
+  pages={56--68},
+  year={1940},
+  publisher={Cambridge University Press}
+}
+@article{curryhoward,
+  title={The formulae-as-types notion of construction},
+  author={Howard, William A},
+  journal={To HB Curry: essays on combinatory logic, lambda calculus and formalism},
+  volume={44},
+  pages={479--490},
+  year={1980}
+}
+@incollection{martinlof,
+  title={An intuitionistic theory of types: Predicative part},
+  author={Martin-L{\"o}f, Per},
+  booktitle={Studies in Logic and the Foundations of Mathematics},
+  volume={80},
+  pages={73--118},
+  year={1975},
+  publisher={Elsevier}
+}
+@incollection{martinlofprog,
+  title={Constructive mathematics and computer programming},
+  author={Martin-L{\"o}f, Per},
+  booktitle={Studies in Logic and the Foundations of Mathematics},
+  volume={104},
+  pages={153--175},
+  year={1982},
+  publisher={Elsevier}
+}
+@phdthesis{coquandcoc,
+  title={The calculus of constructions},
+  author={Coquand, Thierry and Huet, G{\'e}rard},
+  year={1986},
+  school={INRIA}
+}
+@book{coqart,
+  title={Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions},
+  author={Bertot, Yves and Cast{\'e}ran, Pierre},
+  year={2013},
+  publisher={Springer Science \& Business Media}
+}
+@article{dybjer,
+  title={Inductive families},
+  author={Dybjer, Peter},
+  journal={Formal aspects of computing},
+  volume={6},
+  number={4},
+  pages={440--465},
+  year={1994},
+  publisher={Springer}
+}
+@misc{paulincic,
+  title={Introduction to the calculus of inductive constructions},
+  author={Paulin-Mohring, Christine},
+  year={2015},
+  publisher={College Publications}
+}
+@inproceedings{demoura,
+  title={The Lean theorem prover (system description)},
+  author={de Moura, Leonardo and Kong, Soonho and Avigad, Jeremy and Van Doorn, Floris and von Raumer, Jakob},
+  booktitle={International Conference on Automated Deduction},
+  pages={378--388},
+  year={2015},
+  organization={Springer}
+}
+@inproceedings{barrastypedec,
+  title={On the role of type decorations in the calculus of inductive constructions},
+  author={Barras, Bruno and Gr{\'e}goire, Benjamin},
+  booktitle={International Workshop on Computer Science Logic},
+  pages={151--166},
+  year={2005},
+  organization={Springer}
+}
+@article{barrassets,
+  title={Sets in Coq, Coq in sets},
+  author={Barras, Bruno},
+  journal={Journal of Formalized Reasoning},
+  volume={3},
+  number={1},
+  pages={29--48},
+  year={2010}
+}
+@article{coqincoq,
+  title={Coq in coq},
+  author={Barras, Bruno and Werner, Benjamin},
+  journal={Available on the WWW},
+  year={1997},
+  publisher={Citeseer}
+}