Complete Bidirectional Typing for the Calculus of Inductive Constructions
Meven Lennon-Bertrand
This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). It introduces a new judgement intermediate between the usual inference and checking, dubbed constrained inference, to handle the presence of computation in types. The key property of the system is its completeness with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays an important role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is wider, as it gives insights and structure when trying to prove properties on CIC or design variations and extensions. In particular, we put forward constrained inference, an intermediate between the usual inference and checking judgements, to handle the presence of computation in types.
main.tex
\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
%This is a template for producing LIPIcs articles. 
%See lipics-v2021-authors-guidelines.pdf for further information.
%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
%for British hyphenation rules use option "UKenglish", for American hyphenation rules use option "USenglish"
%for section-numbered lemmas etc., use "numberwithinsect"
%for enabling cleveref support, use "cleveref"
%for enabling autoref support, use "autoref"
%for anonymousing the authors (e.g. for double-blind review), add "anonymous"
%for enabling thm-restate support, use "thm-restate"
%for enabling a two-column layout for the author/affiliation part (only applicable for > 6 authors), use "authorcolumns"

\usepackage{style}

\listfiles

%\graphicspath{{./graphics/}}%helpful if your graphic files are in another directory

\bibliographystyle{plainurl}% the mandatory bibstyle

\title{Complete Bidirectional Typing for the Calculus of Inductive Constructions}

\titlerunning{Complete Bidirectional Typing for the Calculus of Inductive Constructions} %optional, please use if title is longer than one line

\author{Meven Lennon-Bertrand}{LS2N, Université de Nantes — Gallinette Project Team, Inria, France \and \url{http://www.meven.ac} }{meven.bertrand@univ-nantes.fr}{}{}%mandatory, please use full name; only 1 author per \author macro; first two parameters are mandatory, other parameters can be empty. Please provide at least the name of the affiliation and the country. The full address is optional

\authorrunning{M. Lennon-Bertrand} %mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'

\Copyright{Meven Lennon-Bertrand} %mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/

\ccsdesc[500]{Theory of computation~Type theory} %mandatory: Please choose ACM 2012 classifications from https://dl.acm.org/ccs/ccs_flat.cfm 

\keywords{Bidirectional Typing, Calculus of Inductive Constructions, Coq, Proof Assistants} % mandatory; please add comma-separated list of keywords

\category{} %optional, e.g. invited paper

\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other repository/website
%\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional

% \supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
\supplementdetails[subcategory = {Formalization}]{Software}{https://github.com/MevenBertrand/metacoq/tree/itp-artefact}
%\supplementdetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93, subcategory={Description, Subcategory}, swhid={Software Heritage Identifier}]{General Classification (e.g. Software, Dataset, Model, ...)}{URL to related version} %linktext, cite, and subcategory are optional

%\funding{(Optional) general funding statement \dots}%optional, to capture a funding statement, which applies to all authors. Please enter author specific funding statements as fifth argument of the \author macro.

\acknowledgements{Many thanks to Matthieu Sozeau for his help with MetaCoq and its nasty inductives, and to Chantal Keller, Nicolas Tabareau and the anonymous reviewers for their helpful comments on earlier versions of this article.}%TODO optional

%\nolinenumbers %uncomment to disable line numbering

%\hideLIPIcs  %uncomment to remove references to LIPIcs series (logo, DOI, ...), e.g. when preparing a pre-final version to be uploaded to arXiv or another public repository

%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\EventEditors{John Q. Open and Joan R. Access}
\EventNoEds{2}
\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
\EventShortTitle{CVIT 2016}
\EventAcronym{CVIT}
\EventYear{2016}
\EventDate{December 24--27, 2016}
\EventLocation{Little Whinging, United Kingdom}
\EventLogo{}
\SeriesVolume{42}
\ArticleNo{23}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
\nolinenumbers

\maketitle

\begin{abstract}
  This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). It introduces a new judgement intermediate between the usual inference and checking, dubbed constrained inference, to handle the presence of computation in types. The key property of the system is its completeness with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays an important role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is wider, as it gives insights and structure when trying to prove properties on CIC or design variations and extensions. In particular, we put forward constrained inference, an intermediate between the usual inference and checking judgements, to handle the presence of computation in types.
\end{abstract}
  
\section{Introduction}

  In logical programming, an important characteristic of judgements is the \emph{mode} of the objects involved, i.e., which ones are considered inputs or outputs. When examining this distinction for a typing judgement $\Gamma \vdash t : T$, both the term $t$ under inspection and the context $\Gamma$ of this inspection are usually known, they are thus inputs (although some depart from this, see \cite{Jim1996}). The mode of the type $T$, however, may vary: should it be inferred based upon $\Gamma$ and $t$, or do we merely want to check whether $t$ conforms to a given $T$? Both are sensible approaches, and in fact typing algorithms for complex type systems usually alternate between them during the inspection of a single term/program. The bidirectional approach makes this difference between modes explicit, by decomposing undirected\footnote{We call anything related to the $\Gamma \vdash t : T$ judgement undirected by contrast with the bidirectional typing.} typing $\Gamma \vdash t : T$ into two separate judgments $\Gamma \vdash t \inferty T$ (inference) and $\Gamma \vdash t \checkty T$ (checking)\footnote{We chose $\inferty$ and $\checkty$ rather than the more usual $\Rightarrow$ and $\Leftarrow$ to avoid confusion with implication on paper, and with the Coq notation for functions in the development.}, that differ only by modes. This decomposition allows theoretical work on practical typing algorithms, but also gives a finer grained structure to typing derivations, which can be of purely theoretical interest even without any algorithm in sight.

  Although this seems appealing, and despite advocacy by McBride \cite{McBride2018,McBride2019} to adopt this approach when designing type systems, most of the theoretical work on dependent typing to this day remains undirected. Others have described on paper bidirectional algorithms for dependent types, starting with Coquand \cite{Coquand1996} and continuing with Norell \cite{Norell2007} or Abel \cite{Abel2017}. However, all of these consider unannotated $\lambda$-abstractions, and use bidirectional typing as a way to remedy this lack of annotations. This is sensible when looking for lightness of the input syntax, but poses an inherent completeness problem, as a term like $(\l x . x)~0$ does not type-check against type $\nat$ in those systems. Very few have considered the case of annotated abstractions, apart from Asperti and the Matita team \cite{Asperti2012}, who however concentrate on specific problems pertaining to unification and implementation of the Matita elaborator, without giving a general bidirectional framework. They also do not consider the problem of completeness with respect to a given undirected system, as it would fail in their setting due to the undecidability of higher order unification.

  Thus, we wish to fill a gap in the literature, by describing a bidirectional type system that is complete with respect to the (undirected) Calculus of Inductive Constructions (CIC). By completeness, we mean that any term that is typable in the undirected system should also infer a type in the bidirectional one. This feature is very desirable when implementing kernels for proof assistants, whose algorithms should correspond to their undirected specification, never missing any typable term. The bidirectional systems we describe thus form intermediate steps between actual algorithms and undirected type systems. This step has proven useful in an ongoing completeness proof of MetaCoq's \cite{Sozeau2020a} type-checking algorithm\footnote{A completeness bug in that algorithm – also present in the Coq kernel – has already been found, see \cref{sec:to-pcuic} for details.}: rather than proving the algorithm complete directly, the idea is to prove it equivalent to the bidirectional type system, separating the implementation problems from the ones regarding the bidirectional structure.
  
  But the interest of having a bidirectional type system equivalent to the undirected one is not limited to the link with algorithms, it is also purely theoretical. First, the structure of a bidirectional derivation is more constrained than that of an undirected one, especially regarding the uses of computation. This finer structure can make proofs easier, while the equivalence ensures that they can be transported to the undirected world. For instance, in a setting with cumulativity/subtyping, the inferred type for a term $t$ should by construction be smaller than any other types against which $t$ checks. This provides an easy proof of the existence of principal types in the undirected system. The bidirectional structure also provides a better base for new type systems. This was actually the starting point for this investigation: in \cite{LennonBertrand2020}, we quickly describe a bidirectional variant of CIC, as the usual undirected CIC is unfit for the gradual extension we envision due to the too high flexibility of a free-standing conversion rule. This is the system we wish to thoroughly describe and investigate here.

  \subparagraph{Outline}
  We start by giving in \cref{sec:ccomega} a general roadmap in the simple setting of pure type systems, including the introduction of a constrained inference judgement that had not been clearly singled out in previous works.
  With the ideas set clear, we go on to the real thing: a bidirectional type system proven equivalent to the Predicative Calculus of Cumulative Inductive Constructions – PCUIC, the extension of CIC nowadays at the heart of Coq. This equivalence has been formalised on top of MetaCoq \cite{Sozeau2020}\footnote{A version frozen as described in this article is available in the following git branch: \url{https://github.com/MevenBertrand/metacoq/tree/itp-artefact}.}
  We next turn back to less technical considerations, as we believe that the bidirectional structure is of general theoretical interest. \Cref{sec:beyond} thus describes the value of basing type systems on the bidirectional system directly rather than on the equivalent undirected one. Finally \cref{sec:related} investigates related work, and in particular tries and identify the implicit presence of constrained inference in various earlier articles, showing how making it explicit clarifies those.


\section{Warming up with \CCo{}}
  \label{sec:ccomega}

\subsection{Undirected \CCo{}}

  As a starting point, let us consider the system \CCo{}. It is the backbone of CIC, and we can already illustrate most of our methodology on it. \CCo{} belongs to the wider class of pure type systems (PTS), that has been thoroughly studied and described, see for instance \cite{Barendregt1992}. Since there are many presentational variations, let us first give a precise account of our conventions. \defemph{Terms} in \CCo{} are given by the grammar
    \begin{mathpar}
    t ::= x \mid \uni[i] \mid \P x : t . t \mid \l x : t . t \mid t~t
    \end{mathpar}
  where the letter $x$ denotes a variable (so will letters $y$ and $z$), and the letter $i$ is an integer (we will also use letters $j$, $k$ and $l$ for those). All other Latin letters will be used for terms, with the upper-case ones used to suggest the corresponding terms should be though of as types — although this is not a syntactical separation. We abbreviate $\P x : A . B$ by $A \to B$ when $B$ does not depend on $x$, as is customary. On those terms, \defemph{reduction} $\red$ is defined as the least congruence such that $(\l x : T . t)~u \red \subs{t}{u}{x}$, where $\subs{t}{u}{x}$ denotes \defemph{substitution}.
  \defemph{Conversion} $\conv$ is the symmetric, reflexive, transitive closure of reduction. Finally, \defemph{contexts} are lists of variable declarations $x : t$ and are denoted using capital Greek letters. We write $\cdot$ for the empty list, $\Gamma, x : T$ for concatenation, and $(x : T) \in \Gamma$ if $(x : T)$ appears in $\Gamma$. Combining those, we can define \defemph{typing} $\Gamma \vdash t : T$ as in \cref{fig:pts-typing}, where $\max{i}{j}$ denotes the maximum of $i$ and $j$.
  We say a context $\Gamma$ is \defemph{well-formed} if $\vdash \Gamma$, a type $T$ is \defemph{well-formed} in a context $\Gamma$ if there exists $i$ such that $\Gamma \vdash T : \uni[i]$, and a term is \defemph{well-formed} in a context $\Gamma$ if there exists $T$ such that $\Gamma \vdash t : T$. We also use \defemph{well-typed} for the latter, and leave the context implicit for the last two when it is clear from context.
  These rules differ from more usual PTS presentations such as \cite{Barendregt1992} on the \nameref{infrule:pts-undir-var} and \nameref{infrule:pts-undir-sort} rules so as to avoid general weakening (which is however admissible) and single out the context well-formedness judgment. Premises are not minimal in order to provide more generous inductive hypotheses when doing proofs by induction on derivations. However, this presentation can easily be seen to be equivalent to that of \cite{Barendregt1992}.

  \begin{figure}
    \begin{mathpar}
      \jformlow{$\vdash \Gamma$}
      \inferrule{ }{\vdash \cdot}[Empty] \label{infrule:pts-undir-empty} \and
      \inferrule{\vdash \Gamma \\ \Gamma \vdash A : \uni[i]}{\vdash \Gamma, x : A}[Ext] \label{infrule:pts-undir-ext} \\
      \jform{$\Gamma \vdash t : T$}
      \inferrule{\vdash \Gamma}{\Gamma \vdash \uni[i] : \uni[i+1]}[Sort] \label{infrule:pts-undir-sort} \and
      \inferrule{\vdash \Gamma \\ (x : A \in \Gamma)}{\Gamma \vdash x : A}[Var] \label{infrule:pts-undir-var} \and
      %\inferrule{\Gamma \vdash x : A \\ \Gamma \vdash B : \uni[i]}{\Gamma, y : B \vdash x : A}[Weak] \label{infrule:pts-undir-weak} \and
      \inferrule{\Gamma \vdash A : \uni[i] \\ \Gamma, x : A \vdash B : \uni[j]}{\Gamma \vdash \P x : A . B : \uni[\max{i}{j}]}[Prod] \label{infrule:pts-undir-prod} \and
      \inferrule{\Gamma \vdash \P x : A . B : \uni[i] \\ \Gamma, x : A \vdash t : B}{\Gamma \vdash \l x : A . t : \P x : A . B}[Abs] \label{infrule:pts-undir-abs} \and
      \inferrule{\Gamma \vdash t : \P x : A . B \\ \Gamma \vdash u : A}{\Gamma \vdash t~u : \subs{B}{u}{x}}[App] \label{infrule:pts-undir-app} \and
      \inferrule{\Gamma \vdash t : A \\ \Gamma \vdash B : \uni[i] \\ A \conv B}{\Gamma \vdash t : B}[Conv] \label{infrule:pts-undir-conv}
    \end{mathpar}

    \caption{Undirected typing for \CCo{}}
    \label{fig:pts-typing}
  \end{figure}

  As any PTS, \CCo{} has many desirable properties. We summarize the ones we rely on here. Detailed proofs in the context of PTS can be found in \cite{Barendregt1992}, and formalisation of the corresponding properties for PCUIC are an important part of MetaCoq.

  \begin{proposition}[Properties of \CCo{}]
    \label{prop:ccomega}
    The type system \CCo{} as just described enjoys the following properties:
    \begin{description}
      \item[Confluence] Reduction $\red$ is confluent. As a direct consequence, two terms are convertible just when they have a common reduct: $t \conv u$ if and only if there exists $t'$ such that $t \rtred t'$ and $u \rtred t'$.
      \item[Transitivity] Conversion is transitive.
      \item[Subject reduction] If $\Gamma \vdash t : T$ and $t \red t'$ then $\Gamma \vdash t' : T$.
      \item[Validity] If $\Gamma \vdash t : T$ then $T$ is well-formed, e.g.\ there exists some $i$ such that $\Gamma \vdash T : \uni[i]$.
    \end{description}
  \end{proposition}

\subsection{Turning \CCo{} Bidirectional}
  \label{sec:ccomega-bidir}

  \subparagraph{McBride’s discipline}
  To design our bidirectional type system, we follow a discipline exposed by McBride \cite{McBride2018,McBride2019}. The central point is to distinguish in a judgment between the subject, whose well-formedness is under scrutiny, from inputs, whose well-formedness is a condition for the judgment to behave well, and outputs, whose well-formedness is a consequence of the judgment. For instance, in inference $\Gamma \vdash t \inferty T$, the subject is $t$, $\Gamma$ is an input and $T$ is an output. This means that one should consider whether $\Gamma \vdash t \inferty T$ only in cases where $\vdash \Gamma$ is already known, and if the judgment is derivable it should be possible to conclude that both $t$ and $T$ are well-formed. All inference rules are to preserve this invariant. This means that inputs to a premise should be well-formed whenever the inputs to the conclusion and outputs and subjects of previous premises are. Similarly the outputs of the conclusion should be well-formed if the inputs of the conclusion and the subjects and outputs of the premises are assumed to be so.
  
  This distinction also applies to the computation-related judgments, although those have no subject. For conversion $T \conv T'$ both $T$ and $T'$ are inputs, and thus should be known to be well-formed beforehand. For reduction $T \rtred T'$, $T$ is an input and $T'$ is an output, so only $T$ needs to be well-formed, with the subject reduction property of the system ensuring that the output $T'$ is also well-formed.
  %\mlb{Would it make sense to use colors in the figure to emphasize mode?}

  \begin{figure}
    \begin{mathpar}
      % \jform{$\vdash \Gamma \checkty$} \\
      % \inferrule{ }{\vdash \cdot \checkty}[Empty] \label{infrule:pts-empty} \and
      % \inferrule{
      %   \vdash \Gamma \checkty \\
      %   \Gamma \vdash T \pinferty{\sorts} s}
      % {\vdash \Gamma, x : T \checkty}[Concat] \label{infrule:pts-concat} \\
    \jform{Inference: $\Gamma \vdash t \inferty T$}
      %
      \inferrule{ }{\Gamma \vdash \uni[i] \inferty \uni[i+1]}[Sort] \label{infrule:pts-sort} \and
      \inferrule{(x : T) \in \Gamma}{\Gamma \vdash x \inferty T}[Var] \label{infrule:pts-var} \and
      \inferrule{\Gamma \vdash A \pinferty{\sorts} \uni[i] \\ \Gamma, x : A \vdash B \pinferty{\sorts} \uni[j]}
        {\Gamma \vdash  \P x : A . B \inferty \uni[\max{i}{j}]}[Prod] \label{infrule:pts-prod} \\ 
      \inferrule{\Gamma \vdash A \pinferty{\sorts} \uni[i] \\ \Gamma, x : A \vdash t \inferty B}
        {\Gamma \vdash \l x : A . t \inferty  \P x : A . B}[Abs] \label{infrule:pts-abs} \and
      \inferrule{\Gamma \vdash t \pinferty{\Pi}  \P x : A . B \\ \Gamma \vdash u \checkty A}
        {\Gamma \vdash t~u \inferty \subs{B}{u}{x}}[App] \label{infrule:pts-app} \\
%
    \jformlow{Checking: $\Gamma \vdash t \checkty T$} 
%
    \inferrule{\Gamma \vdash t \inferty T' \\ T' \conv T}
      {\Gamma \vdash t \checkty T}[Check] \label{infrule:pts-check} \\
%
    \jform{Constrained inference: $\Gamma \vdash t \pinferty{h} T$}
%
    \inferrule{\Gamma \vdash t \inferty T \\ T \rtred \uni[i]}
      {\Gamma \vdash t \pinferty{\sorts} \uni[i]}[Sort-Inf] \label{infrule:pts-sort-inf} \and
    \inferrule{\Gamma \vdash t \inferty T \\ T \rtred \P x : A. B}
      {\Gamma \vdash t \pinferty{\P} \P x : A . B}[Prod-Inf] \label{infrule:pts-prod-inf}
  \end{mathpar}
  
  \caption{Bidirectional typing for \CCo{}}
  \label{fig:bidir-pts}
  \end{figure}

  \subparagraph{Constrained inference}
  Beyond the already described inference and checking judgements another one appears in the bidirectional typing rules of \cref{fig:bidir-pts}: \defemph{constrained inference}, written $\Gamma \vdash t \pinferty{h} T$, where $h$ is either $\Pi$ or $\sorts$  – and will be extended once we introduce more type formers. Constrained inference is a judgement – or, rather, a family of judgements indexed by $h$ – with the exact same modes as inference, but where the type output is not completely free. Rather, as the name suggests, a constraint is imposed on it, namely that its head constructor can only be the corresponding element of $h$. This is needed to handle the behaviour absent in simple types that some terms might not have a desired type “on the nose”, as exemplified by the first premise $\Gamma \vdash t \pinferty{\Pi} \P x : A . B$ of the \nameref{infrule:pts-app} rule for $t~u$. Indeed, it would be too much to ask $t$ to directly infer a $\Pi$-type, as some reduction might be needed on $T$ to uncover this $\Pi$. Checking also cannot be used, because the domain and codomain of the tentative $\Pi$-type are not known at that point: they are to be inferred from $t$.

  \subparagraph{Structural rules}
  To transform the rules of \cref{fig:pts-typing} to those of \cref{fig:bidir-pts}, we start by recalling that we wish to obtain a complete bidirectional type system. Therefore any term should infer a type, and thus all structural rules (i.e.\ all rules where the subject of the conclusion starts with a term constructor) should give rise to an inference rule. It thus remains to choose the judgements for the premises, which amounts to determining their modes. If a term in a premise appears as input in the conclusion or output of a previous premise, then it can be considered an input, otherwise it must be an output. Moreover, if a type output is unconstrained, then inference can be used, otherwise we must resort to constrained inference.
  
  This applies straightforwardly to most rules but the PTS-style \nameref{infrule:pts-undir-abs}. Indeed, neither $\Gamma \vdash \P x : A . B : \uni[i]$ nor $\Gamma, x : A \vdash t : B$ can be taken as the first bidirectional premise: the first one because $B$ is not known from inputs to the conclusion, and the second because context $\Gamma, x : A$ is not known to be well-formed from the conclusion. For general PTS, this is quite problematic, as demonstrated by Pollack \cite{Pollack1992}. For \CCo{}, however, the solution is simple. Replacing $\Gamma \vdash \P x : A . B : \uni[i]$ by the equivalent $\Gamma \vdash A : \uni[j]$ and $\Gamma, x : A \vdash B : \uni[j']$, the former can become the first premise, ensuring that type inference for $t$ is done in a well-formed context, and the latter can be dropped based upon the invariant that outputs – here the type $B$ inferred for $t$ — are well-formed.

  Similarly, as the context is always supposed to be well-formed as an input to the conclusion, it is not useful to re-check it, and thus the premise of \nameref{infrule:pts-undir-sort} and \nameref{infrule:pts-undir-var} can be safely dropped. This is in line with implementations, where the context is not re-checked at leaves of a derivation tree, with performance issues in mind. The well-formedness invariants then ensure that any derivation starting with the (well-formed) empty context will only handle well-formed contexts.

  \subparagraph{Computation rules}
  We are now left with the non-structural conversion rule. As we observed, there are two possible modes for computation: if both sides are inputs, conversion can be used, but if only one is known one must resort to reduction, and the other side becomes an output instead. Rule \nameref{infrule:pts-check} corresponds to the first case, while rules \nameref{infrule:pts-prod-inf} and \nameref{infrule:pts-sort-inf} both are in the second case. This difference in turn introduces the need to separate between checking, that calls for the first rule, and constrained inference, that requires the others.

  The need to split the conversion rule into a (weak-head) reduction and conversion subroutine depending on the mode is known to the implementors of proof assistants \cite{Abel2011}. However, we wish to de-emphasize the role devoted specifically to reduction in the description of those algorithms, instead putting constrained inference forward. Indeed, reduction is only a means to determine whether a certain term fits into a certain category of types. In the setting of \CCo{}, there is mainly one way to do so, which is to reduce its type until its head constructor is exposed.
  However, as soon as conversion is extended, for instance with unification \cite{Asperti2012}, coercions \cite{Asperti2012,Sozeau2007} or graduality \cite{LennonBertrand2020}, reduction is not enough any more. Singling out constrained inference then makes the required modification to the typing rules clearer. We come back to this more in length in \cref{sec:rel-constrained}.

\subsection{Properties}

  Let us now state the two main properties relating the bidirectional system to the undirected one: it is both correct (terms typable in the bidirectional system are typable in the undirected system) and complete (all terms typable in the undirected system are also typable in the bidirectional system).

\subsubsection{Correctness}

  A bidirectional derivation can be seen as a refinement of an undirected derivation. Indeed, the bidirectional structure can be erased – replacing each bidirectional rule with the corresponding undirected rule – to obtain an undirected derivation, but for missing sub-derivations, which can be retrieved using the invariants on well-formedness of inputs and outputs. Thus, we get the following correctness theorem – note how McBride’s discipline manifests as well-formedness hypothesis on inputs.

  \begin{theorem}[Correctness of bidirectional typing for \CCo{}]
    \label{thm:corr-ccomega}
    If $\Gamma$ is well-formed and $\Gamma \vdash t \inferty T$ or $\Gamma \vdash t \pinferty{h} T$ then $\Gamma \vdash t : T$. If $\Gamma$ and $T$ are well-formed and $\Gamma \vdash t \checkty T$ then $\Gamma \vdash t : T$. 
  \end{theorem}
  
  \begin{proof}
    The proof is by mutual induction on the bidirectional typing derivation.

    Each rule of the bidirectional system can be replaced by the corresponding rule of the undirected system, with all three \nameref{infrule:pts-check}, \nameref{infrule:pts-prod-inf} and \nameref{infrule:pts-sort-inf} replaced by \nameref{infrule:pts-undir-conv}, \nameref{infrule:pts-abs} using an extra \nameref{infrule:pts-undir-prod} rule. In all cases, the induction hypothesis can be used on sub-derivations of the bidirectional judgment because the context extensions and checking are done with types that are known to be well-formed by induction hypothesis on previous premises and validity.

    Some sub-derivations of the undirected rules that have no counterpart in the bidirectional ones are however missing. In rules \nameref{infrule:pts-sort} and \nameref{infrule:pts-var} the hypothesis that $\vdash \Gamma$ is enough to get the required premise. For rule \nameref{infrule:pts-check}, the well-formedness hypothesis on the type is needed to get the second premise of rule \nameref{infrule:pts-undir-conv}. As for \nameref{infrule:pts-prod-inf} and \nameref{infrule:pts-sort-inf}, that second premise is obtained using the induction hypothesis, validity and subject reduction. Finally, the missing premise on the codomain of the product type in rule \nameref{infrule:pts-abs} is obtained by validity. 
    
    Uses of validity could alternatively be handled by strengthening the theorem to incorporate the well-formedness of types when they are outputs.

  \end{proof}

\subsubsection{Completeness}

  Let us now state the most important property of our bidirectional system: it does not miss any undirected derivation.

  \begin{theorem}[Completeness of bidirectional typing for \CCo{}]
    \label{thm:compl-ccomega}
    If $\Gamma \vdash t : T$ then there exists $T'$ such that $\Gamma \vdash t \inferty T'$ and $T' \conv T$.
  \end{theorem}

  \begin{proof}
    The proof is by induction on the undirected typing derivation.
    
    Rules \nameref{infrule:pts-undir-sort} and \nameref{infrule:pts-undir-var} are base cases, and can be replaced by the corresponding rules in the bidirectional world. Rule \nameref{infrule:pts-undir-conv} is a direct consequence of the induction hypothesis on its first premise, together with transitivity of conversion.
    
    For rule \nameref{infrule:pts-undir-prod}, we need the intermediate lemma that if $T$ is a term such that $T \conv \uni[i]$, then also $T \rtred \uni[i]$. This is a consequence of confluence of reduction. In turn, it implies that if $\Gamma \vdash t \inferty T$ and $T \conv \uni[i]$ then $\Gamma \vdash t \pinferty{\sorts} \uni[i]$, and is enough to conclude for that rule.
    
    In rule \nameref{infrule:pts-undir-abs}, the induction hypothesis gives $\Gamma \vdash \P x : A . B \inferty T$ for some $T$, and an inversion on this gives $\Gamma \vdash A \pinferty{\uni} \uni[i]$ for some $i$. Combined with the second induction hypothesis, we get $\Gamma \vdash \l x : A . t \inferty \P x : A . B'$ for some $B'$ such that $B \conv B'$, and thus $\P x : A . B \conv \P x : A . B'$ as desired.

    We are finally left with the \nameref{infrule:pts-undir-app} rule. We know that $\Gamma \vdash t \inferty T$ with $T \conv \P x : A . B$. Confluence then implies that $T \rtred \P x : A' . B'$ for some $A'$ and $B'$ such that $A \conv A'$ and $B \conv B'$. Thus $\Gamma \vdash t \pinferty{\Pi} \P x : A' . B'$. But by induction hypothesis we also know that $\Gamma \vdash u \inferty A''$ with $A'' \conv A$ and so by transitivity of conversion $\Gamma \vdash u \checkty A'$. We can thus apply \nameref{infrule:pts-app} to conclude.

  \end{proof}

  Contrarily to correctness, which kept a similar derivation structure, completeness is of a different nature. Because in bidirectional derivations the conversion rules are much less liberal than in undirected derivations, the crux of the proof is to ensure that conversions can be permuted with structural rules, in order to concentrate them in the places where they are authorized in the bidirectional derivation. In a way, composing completeness with conversion gives a kind of normalization procedure that produces a canonical undirected derivation by pushing all conversions down as much as possible.

\subsubsection{Reduction strategies}

  The judgements of \cref{fig:bidir-pts} are syntax-directed, in the sense that there is always at most one rule that can be used to derive a certain typing judgements. But with the rules as given there is still some indeterminacy. Indeed when appealing to reduction no strategy is fixed, thus two different reducts give different uses of the rule, resulting in different inferred types – although those are still convertible. However, a reduction strategy can be imposed to completely eliminate indeterminacy in typing, leading to the following.
  
  \begin{proposition}[Reduction strategy]
    \label{prop:red-strat}

    If $\rtred$ is replaced by weak-head reduction in rules \nameref{infrule:pts-sort-inf} and \nameref{infrule:pts-prod-inf}, then given a well-formed context $\Gamma$ and a term $t$ there is at most one derivation of $\Gamma \vdash t \inferty T$ and $\Gamma \vdash t \pinferty{h} T$, and so in particular such a $T$ is unique. Similarly, given well-formed $\Gamma$ and $T$ and a term $t$ there is at most one derivation of $\Gamma \vdash t \checkty T$.
    Moreover, the existence of those derivations is decidable.
  \end{proposition}

  The algorithm for deciding the existence of the derivations is straightforward from the bidirectional rules, it amounts to structural recursion on the subject.

\section{From \CCo{} to PCUIC}
  \label{sec:to-pcuic}
  
  \CCo{} is already a powerful system, but today’s proof assistants rely on much more complex features. There are two main areas of differences between \CCo{} and the Predicative Calculus of Cumulative Inductive Constructions (PCUIC), the type theory nowadays behind the Coq proof assistant. Adapting to those is a good stress test for the bidirectional approach: seamlessly doing so is a good sign that the general methodology we presented is robust.

  The first area of difference are the universes. While on paper those are simply integer, to handle typical ambiguity and polymorphic (co)-inductive types, PCUIC uses algebraic universes, containing level variables, algebraic $\vee$ and $+1$ operators, and a special level for the sort Prop. Moreover, those universes are cumulative, that is they behave as if smaller universes were included in larger ones. The precise handling of the algebraic universes is abstracted away in MetaCoq, and quite similar in the directed and undirected systems, so it did not prove too difficult to handle. Cumulativity, however, introduces some not-so-small differences with the previous presentation, so we spend some time on it in \cref{sec:pcuic-cumul}.

  The second is the addition of new base type and term constructors. We describe the treatment of inductive types in \cref{sec:pcuic-indu}. Co-inductive types and records behave very similarly to inductive types at the level of typing, so we do not dwell on them. The difference lies mainly at the level of reduction/conversion, but as our type system treats those as black boxes the differences have a negligible impact.
  
  The interplay between those two areas is quite subtle, and we were able to uncover an incompleteness bug in the current kernel of Coq regarding pattern-matching of cumulative inductive types. This bug had gone unnoticed until our formalisation, but was causing subject reduction failures in some corner cases\footnote{The precise issue in the kernel is described in this git issue: \url{https://github.com/coq/coq/issues/13495}.}. We try and give an intuition of the problem in \cref{sec:pcuic-indu}.

\subsection{Cumulativity}
\label{sec:pcuic-cumul}

  PCUIC incorporates a limited form of subtyping, corresponding to the intuition that smaller universes are included in larger ones. Conversion $\conv$ is therefore replaced by \defemph{cumulativity} $\cumul$, the main difference being that the constraint on universes is relaxed. For conversions $\uni[i] \conv \uni[j]$ only when $i = j$, but for cumulativity $\uni[i] \cumul \uni[j]$ whenever $i \leq j$ – and this extends by congruence through most constructors. The conversion rule is accordingly replaced by the following cumulativity rule
  \begin{mathpar}
    \inferrule{\Gamma \vdash t : A \\ \Gamma \vdash B : \uni[i] \\ A \cumul B }{\Gamma \vdash t : B}[Cumul] \label{infrule:pcuic-undir-cumul}
  \end{mathpar}
  This reflects the view that universes $\uni[i]$ should be included one in the next when going up in the hierarchy. In \CCo{}, all types for a given term $t$ in a fixed context $\Gamma$ are equally good, as they are all convertible. This is not the case any more in presence of cumulativity, as we can have $T \cumul T'$ but not $T \conv T'$. Of particular interest are principal types, defined as follows.

  \begin{definition}[Principal type]
    The term $T$ is called a \defemph{principal type} for term $t$ in context $\Gamma$ if it is a least type for $t$ in $\Gamma$, that is if $\Gamma \vdash t : T$ and for any $T'$ such that $\Gamma \vdash t : T'$ we have $T \cumul T'$.
  \end{definition}

  The existence of such principal types is no so easy to prove directly but quite useful, as they are in a sense the best types for any terms. Indeed, if $T$ is a principal type for $t$ in $\Gamma$ and $T'$ is any other type for $t$, the \nameref{infrule:pcuic-undir-cumul} rule can be used to deduce $\Gamma \vdash t : T'$ from $\Gamma \vdash t : T$, which in general is not the case if $T$ is not principal. Similarly, if $T$ and $T'$ are two types for a term $t$, then they are not directly related, but the existence of principal types ensures that there exists some $T''$ that is a type for $t$ and such that $T \cumul T'$ and $T \cumul T''$, indirectly relating $T'$ and $T''$.

  Reflecting this modification in the bidirectional system of course calls for an update to the computation rules. The change to the \nameref{infrule:pts-check} rule is direct: simply replace conversion with cumulativity.
  \begin{mathpar}
    \inferrule{\Gamma \vdash t \inferty A \\ A \cumul B }{\Gamma \vdash t \checkty B}[Cumul] \label{infrule:pcuic-cumul}
  \end{mathpar}
  As to the constrained inference rules, there is no need to modify them. Intuitively, this is because there is no reason to degrade a type to a larger one when it is not needed. We only resort to cumulativity when it is forced by a given input. In that setting, completeness becomes the following:

  \begin{theorem}[Completeness with cumulativity]
    \label{thm:comp-cumul}
    If $\Gamma \vdash t : T$ using rules of \cref{fig:pts-typing} replacing \nameref{infrule:pts-undir-conv} with \nameref{infrule:pcuic-undir-cumul}, then $\Gamma \vdash t \inferty T'$ is derivable with rules of \cref{fig:bidir-pts} replacing \nameref{infrule:pts-check} with \nameref{infrule:pcuic-cumul} for some $T'$ such that $T' \cumul T$.
  \end{theorem}

  In that setting, even without fixing a reduction strategy as in \cref{prop:red-strat}, there is a weaker uniqueness property for inferred types.

  \begin{proposition}[Uniqueness of inferred type]
    \label{prop:unique-inf}
    If $\Gamma$ is well-formed, $\Gamma \vdash t \inferty T$ and $\Gamma \vdash t \inferty T'$ then $T \conv T'$. Similarly if $\Gamma$ is well-formed, $\Gamma \vdash t \pinferty{h} T$ and $\Gamma \vdash t \pinferty{h} T'$ then $T \conv T'$.
  \end{proposition}

  \begin{proof}
    Mutual induction on the first derivation. It is key that constrained inference rules only reduce a type, so that the type in the conclusion is convertible to the type in the premise, rather than merely related by cumulativity.
  \end{proof}
  
  In particular, combining those two properties with a correctness property akin to \cref{thm:corr-ccomega}, we can prove that any inferred type is principal, and so that they both exist and are computable since the bidirectional judgement can still be turned into an algorithm in the spirit of \cref{prop:red-strat}.

  \begin{proposition}[Principal types]
    \label{prop:princ-types}
    If $\Gamma$ is well-formed and $\Gamma \vdash t \inferty T$ then $T$ is a principal type for $t$ in $\Gamma$.
  \end{proposition}

  \begin{proof}
    If $\Gamma \vdash t : T'$, then by completeness there exists some $T''$ such that $\Gamma \vdash t \inferty T''$ and moreover $T'' \cumul T'$. But by uniqueness $T \conv T'' \cumul T'$ and thus $T \cumul T'$, and $T$ is indeed a principal type for $t$ in $\Gamma$.
  \end{proof}

  Reasoning on the bidirectional derivation thus makes proofs easier, while the correctness and completeness properties ensure they can be carried to the undirected system. Another way to understand this is that seeing completeness followed by correction as a normalization procedure on derivations, the produced canonical derivation is more structured and thus more amenable to proofs. Here for instance the uniqueness of the inferred type translates to the existence of principal types via correctness, and the normalization of the derivations optimizes it to derive a principal type.

\subsection{Inductive Types}
\label{sec:pcuic-indu}

  \begin{figure}[th]
    
    \begin{mathpar}
  %     \inferrule{\vdash \Gamma}{\Gamma \vdash \nat : \uni[0]} \and
  %     \inferrule{\vdash \Gamma}{\Gamma \vdash \zero : \nat} \and
  %     \inferrule{\vdash \Gamma}{\Gamma \vdash \succ : \nat \to \nat} \and
  %     \inferrule{
  %       \Gamma, x : \nat \vdash P : \uni[i] \\
  %       \Gamma \vdash p_{\zero} : \subs{P}{\zero}{x} \\
  %       \Gamma, n : \nat, p : \subs{P}{n}{x} \vdash p_{\succ} : \subs{P}{\succ[n]}{x} \\
  %       \Gamma \vdash s : \nat }
  %       {\Gamma \vdash \indnat{s}{x.P}{p_{\zero}}{p_{\succ}} : \subs{P}{s}{x}} \\
  %     %
      \inferrule{\Gamma \vdash A : \uni[i] \\ \Gamma, x : A \vdash B : \uni[j]}{\Gamma \vdash \S x : A . B : \uni[\max{i}{j}]}[$\S$-type] \label{infrule:undir-sig-type} \and
      \inferrule{\Gamma \vdash A : \uni[i] \\ \Gamma, x : A \vdash B : \uni[j] \\
        \Gamma \vdash a : A \\ \Gamma \vdash b : \subs{B}{a}{x}}{\Gamma \vdash \pair{x}{A}{B}{a}{b} : \S x : A . B}[$\S$-cons] \label{infrule:undir-sig-cons} \and
      \inferrule{
        \Gamma, z : \S x : A . B \vdash P : \uni[i] \\
        \Gamma, x : A, y : B \vdash b : \subs{P}{(x,y)}{z} \\
        \Gamma \vdash s : \S x : A . B }
        {\Gamma \vdash \indS{z.P}{x.y.p}{s} : \subs{P}{s}{z}}[$\S$-rec] \label{infrule:undir-sig-rec} \\
  %     %
  %     \inferrule{\Gamma \vdash A : \uni[i] \\ \Gamma \vdash a : A \\ \Gamma \vdash a' : A}{\Gamma \vdash \eq{A}{a}{a'} : \uni[i]} \and
  %     \inferrule{\Gamma \vdash A : \uni[i] \\ \Gamma \vdash a : A}{\Gamma \vdash \refl{A}{a} : \eq{A}{a}{a}} \and
  %     \inferrule{
  %       \Gamma, x : A, y : \eq{A}{a}{x} \vdash P : \uni[i] \\
  %       \Gamma \vdash p : \subs{\subs{P}{\refl{A}{a}}{y}}{a}{x} \\
  %       \Gamma \vdash s : \eq{A}{a}{a'} }
  %       {\Gamma \vdash \indeq{s}{x.y.P}{p} : \subs{\subs{P}{s}{y}}{a'}{x}}
    \end{mathpar}

    \caption{Undirected sum type}
    \label{fig:undir-indu}
  \end{figure}

  \begin{figure}[th]
    
    \begin{mathpar}
      \jformlow{$\Gamma \vdash t \inferty T$}
      % \inferrule{ }{\Gamma \vdash \nat \inferty \uni[0]} \and
      % \inferrule{ }{\Gamma \vdash \zero \inferty \nat} \and
      % \inferrule{ }{\Gamma \vdash \succ \inferty \nat \to \nat} \and
      % \inferrule{
      %   \Gamma \vdash s \pinferty{\nat} \nat \\
      %   \Gamma, x : \nat \vdash P \pinferty{\uni} \uni[i] \\
      %   \Gamma \vdash p_{\zero} \checkty \subs{P}{\zero}{x} \\
      %   \Gamma, n : \nat, p : \subs{P}{n}{x} \vdash p_{\succ} \checkty \subs{P}{\succ[n]}{x} }
      %   {\Gamma \vdash \indnat{x.P}{p_{\zero}}{p_{\succ}{s}} \inferty \subs{P}{s}{x}} \\
      %
      \inferrule{\Gamma \vdash A \pinferty{\uni} \uni[i] \\ \Gamma, x : A \vdash B \pinferty{\uni} \uni[j]}{\Gamma \vdash \S x : A . B \inferty \uni[\max{i}{j}]}[$\S$-type] \label{infrule:sig-type} \and
      \inferrule{\Gamma \vdash A \pinferty{\uni} \uni[i] \\ \Gamma, x : A \vdash B \pinferty{\uni} \uni[j] \\
        \Gamma \vdash a \checkty A \\ \Gamma \vdash b \checkty \subs{B}{a}{x}}{\Gamma \vdash \pair{x}{A}{B}{a}{b} \inferty \S x : A . B}[$\S$-cons] \label{infrule:sig-cons} \and
      \inferrule{
        \Gamma \vdash s \pinferty{\S} \S x : A . B \\
        \Gamma, z : \S x : A . B \vdash P \pinferty{\uni} \uni[i] \\
        \Gamma, x : A, y : B \vdash b \checkty \subs{P}{(x,y)}{z} }
        {\Gamma \vdash \indS{z.P}{x.y.b}{s} \inferty \subs{P}{s}{z}}[$\S$-rec] \label{infrule:sig-rec} \\
      %
      % \inferrule{\Gamma \vdash A \pinferty{\uni} \uni[i] \\ \Gamma \vdash a \checkty A \\ \Gamma \vdash a' \checkty A}{\Gamma \vdash \eq{A}{a}{a'} \inferty \uni[i]} \and
      % \inferrule{\Gamma \vdash A \pinferty{\uni} \uni[i] \\ \Gamma \vdash a \checkty A}{\Gamma \vdash \refl{A}{a} \inferty \eq{A}{a}{a}} \and
      % \inferrule{
      %   \Gamma \vdash s \inferty \eq{A}{a}{a'} \\
      %   \Gamma, x : A, y : \eq{A}{a}{x} \vdash P \pinferty{\uni} \uni[i] \\
      %   \Gamma \vdash p \checkty \subs{\subs{P}{\eq{A}{a}{a}}{y}}{a}{x} }
      %   {\Gamma \vdash \indeq{x.y.P}{p}{s} \inferty \subs{\subs{P}{s}{y}}{a'}{x}} \\
      %
      \jformlow{$\Gamma \vdash t \pinferty{h} T$}
      % \inferrule{\Gamma \vdash t \inferty T \\ T \rtred \nat}{\Gamma \vdash t \pinferty{\nat} \nat} \and
      \inferrule{\Gamma \vdash t \inferty T \\ T \rtred \S x : A . B}{\Gamma \vdash t \pinferty{\S} \S x : A . B}[$\S$-Inf] \label{infrule:sig-inf} \and
      % \inferrule{\Gamma \vdash t \inferty T \\ T \rtred \eq{A}{a}{a'}}{\Gamma \vdash t \pinferty{\eqind} \eq{A}{a}{a'}}
    \end{mathpar}

    \caption{Bidirectional sum type}
    \label{fig:bidir-indu}
  \end{figure}

  \subparagraph{Sum type}

  Before we turn to the general case of inductive types of the formalisation, let us present a simple inductive type: dependent sums. The undirected rules are given in \cref{fig:undir-indu}, and are inspired from the theoretical presentation of such dependent sums, such at the one of the Homotopy Type Theory book \cite{UniFoundationsProgram2013}. In particular, we use the same convention to write $y.P$ when variable $y$ is bound in $P$. Note however that contrarily to \cite{UniFoundationsProgram2013}, some typing information is kept on the pair constructor. Exactly as for the abstraction, this is to be able to infer a unique, most general type in the bidirectional system. Indeed, without that information a pair $(a,b)$ could inhabit multiple types $\S x : A . B$ because there are potentially many incomparable types $B$ such that $\subs{B}{a}{x}$ is a type for $b$, as even if $\subs{B}{a}{x}$ and $\subs{B'}{a}{x}$ are convertible $B$ and $B'$ may be quite different, depending of which instances of $a$ in $\subs{B}{a}{x}$ are abstracted to $x$.

  To obtain the bidirectional rules of \cref{fig:bidir-indu}, first notice that all undirected rules are structural and must thus become inference rules if we want the resulting system to be complete, just as in \cref{sec:ccomega}. The question therefore is again to know which modes to choose for the premises. For \nameref{infrule:undir-sig-type} and \nameref{infrule:sig-cons} this is straightforward: when the type appears in the conclusion, use checking, otherwise (constrained) inference. The case of the destructors is somewhat more complex. Handling the subterms of the destructor in the order in which they usually appear (predicate, branches and finally scrutinee) is not possible, as the parameters of the inductive type are needed to construct the context in which the predicate is typed. However those parameters can be inferred from the scrutinee. Thus, a type for the scrutinee is first obtained using a new constrained inference judgment, forcing the inferred type to be a $\S$-type, but leaving its parameters free. Next, the obtained arguments can be used to construct the context to type the predicate. Finally, once the predicate is known to be well-formed, it can be used to type-check the branch. 
  
  \begin{figure}[th]
    
    \begin{mathpar}
      \jformlow{$\Gamma \vdash t \inferty T$}
      \inferrule{ }{\Gamma \vdash \nat \inferty \uni[0]} \and
      \inferrule{ }{\Gamma \vdash \zero \inferty \nat} \and
      \inferrule{\Gamma \vdash n \checkty \nat }{\Gamma \vdash \succ[n] \inferty \nat} \and
      \inferrule{
        \Gamma \vdash s \pinferty{\nat} \nat \\
        \Gamma, z : \nat \vdash P \pinferty{\uni} \uni[i] \\
        \Gamma \vdash b_{\zero} \checkty \subs{P}{\zero}{z} \\
        \Gamma, x : \nat, p : \subs{P}{x}{z} \vdash b_{\succ} \checkty \subs{P}{\succ[x]}{z} }
        {\Gamma \vdash \indnat{z.P}{b_{\zero}}{x.p.b_{\succ}}{s} \inferty \subs{P}{s}{z}} \\
      %
      \inferrule{\Gamma \vdash A \pinferty{\uni} \uni[i] \\ \Gamma \vdash a \checkty A \\ \Gamma \vdash a' \checkty A}{\Gamma \vdash \eq{A}{a}{a'} \inferty \uni[i]} \and
      \inferrule{\Gamma \vdash A \pinferty{\uni} \uni[i] \\ \Gamma \vdash a \checkty A}{\Gamma \vdash \refl{A}{a} \inferty \eq{A}{a}{a}} \and
      \inferrule{
        \Gamma \vdash s \inferty \eq{A}{a}{a'} \\
        \Gamma, x : A, z : \eq{A}{a}{x} \vdash P \pinferty{\uni} \uni[i] \\
        \Gamma \vdash b \checkty \subs{\subs{P}{\eq{A}{a}{a}}{z}}{a}{x} }
        {\Gamma \vdash \indeq{x.z.P}{b}{s} \inferty \subs{\subs{P}{s}{z}}{a'}{x}} \\
      
      \jformlow{$\Gamma \vdash t \pinferty{h} T$}
      \inferrule{\Gamma \vdash t \inferty T \\ T \rtred \nat}{\Gamma \vdash t \pinferty{\nat} \nat} \and
      \inferrule{\Gamma \vdash t \inferty T \\ T \rtred \eq{A}{a}{a'}}{\Gamma \vdash t \pinferty{\eqind} \eq{A}{a}{a'}}
    \end{mathpar}

    \caption{Other bidirectional inductive types}
    \label{fig:bidir-indu-other}
  \end{figure}

  This same approach can be readily extended to other usual inductive types, with recursion or indices posing no specific problems, see \cref{fig:bidir-indu-other}. The choice to use $\pinferty{\uni}$ rather than $\checkty$ for types is guided by the intuition that the universe level of e.g.\ $A$ in $\eq{A}{a}{a'}$ is free, similarly to what happens for sum types.
  
  \begin{figure}
    \begin{mathpar}
      \jform{$\Gamma \vdash t \inferty T$}
      %
      \inferrule{ }
      {\Gamma \vdash I\ulev{\lis{i}} \inferty \P (\lis{x} : \lis{X}\ulev{\lis{i}}) (\lis{y} : \lis{Y}\ulev{\lis{i}}), \uni[l\ulev{\lis{i}}]}[Ind] \label{infrule:indu-indu}\and
      \inferrule{ }
      {\Gamma \vdash c_k\ulev{\lis{i}} \inferty \P (\lis{x} : \lis{X}\ulev{\lis{i}}) (\lis{y} : \lis{Y_k}\ulev{\lis{i}}), I\ulev{\lis{i}}~\lis{x}~\lis{u_k\ulev{\lis{i}}} }[Cons] \label{infrule:indu-cons} \and
      %		
      \inferrule{
        \Gamma \vdash s \pinferty{I} I\ulev{\lis{i'}}~\lis{a}~\lis{b} \\
        \Gamma \vdash \lis{p}_k \checkty \subs{\lis{X}_k}{\lis{p}}{\lis{x}} \\
        \Gamma, \lis{y} : \subs{\lis{Y}\ulev{\lis{i}}}{\lis{p}}{\lis{x}}, z : I\ulev{\lis{i}}~\lis{p}~\lis{y} \vdash P \pinferty{\uni} \uni[j] \\
        I\ulev{\lis{i'}}~\lis{a}~\lis{b} \cumul I\ulev{\lis{i}}~\lis{p}~\lis{b} \\
        \Gamma, \lis{y} : \subs{\lis{Y_k}\ulev{\lis{i}}}{\lis{p}}{\lis{x}} \vdash \lis{t}_k \checkty \subs{\subs{P}{c_k\ulev{\lis{i}}~\lis{p}~\lis{y}}{z}}{\lis{u_k}\ulev{\lis{i}}}{\lis{y}}  
      }{\Gamma \vdash \match{s}{(I,\lis{i},\lis{p})}{P}{\lis{t}} \inferty \subs{\subs{P}{s}{z}}{\lis{b}}{\lis{y}}}[Match] \label{infrule:indu-match} \and
      %		
      \inferrule{
        \Gamma \vdash T \pinferty{\uni} \uni[i] \\
        \Gamma, f : T \vdash t \checkty T \\
        \text{ guard condition}
      }{\Gamma \vdash \fix{f}{T}{t} \inferty T}[Fix] \label{infrule:indu-fix} \\

      \jformlow{$\Gamma \vdash t \pinferty{I} T $}
        \inferrule{
          \Gamma \vdash t \inferty T \\
          T \red I~\lis{a}~\lis{b}
        }{\Gamma \vdash t \pinferty{I} I~\lis{a}~\lis{b}}

    \end{mathpar}

    \caption{Bidirectional inductive type – PCUIC style}
    \label{fig:bidir-indu-pcuic}
  \end{figure}
  

  \subparagraph{Polymorphic, Cumulative Inductive Types} 
  
  The account of general inductive types in PCUIC is quite different from the one we just gave. The main addition is universe polymorphism \cite{Sozeau2014}, which means that inductive types and constructors come with explicit universe levels. The $\S$-type of the previous paragraph, for instance, would contain an explicit universe level $i$, and both $A$ and $B$ would be checked against $\uni[i]$ rather than having their level inferred. This makes the treatment of complex inductive types possible by using checking uniformly – rather than relying on constrained inference to infer universe levels – at the cost of possibly needless annotations, as here with $\S$-types.
  To make that polymorphism more seamless, those polymorphic inductive types are also cumulative \cite{Timany2018}: in much the same way as $\uni[i] \cumul \uni[j]$ if $i \leq j$, also $\nat\ulev{i} \cumul \nat\ulev{j}$, where $\nat\ulev{i}$ denotes the polymorphic inductive $\nat$ at universe level $i$. This enables lifting from a lower universe to a higher one, so that for instance $\vdash 0\ulev{i} : \nat\ulev{j}$ if $i \leq j$.
  PCUIC as presented in MetaCoq also presents constructors and inductive types as functions, rather than requiring them to be fully applied, and it separates recursors into a pattern-matching and a fixpoint construct, the latter coming with a specific guard condition to keep the normalization property enjoyed by a system with recursors.

  A sketch of the bidirectional rules is given in \cref{fig:bidir-indu-pcuic}, for a generic inductive $I$.
  We use bold characters to denote lists – for instance $\lis{a}$ is a list of terms – and indexes to denote a specific element – so that $\lis{a}_k$ is the $k$-th element of the previous. The considered inductive $I$ has parameters of type $\lis{X}$, indices of type $\lis{Y}$ and inhabits some universe $\uni[l]$. Its constructors $c_k$ are of types $\P (\lis{x} : \lis{X}) (\lis{y} : \lis{Y_k}), I~\lis{x}~\lis{u}$, with $\lis{u_k}$ terms possibly depending on both $\lis{x}$ and $\lis{y}$. Since we are considering a polymorphic inductive type, all of those actually have to be instantiate with universe levels, an operation we denote with $\ulev{\lis{i}}$.
  
  The two rules \nameref{infrule:indu-indu}, \nameref{infrule:indu-cons} are similar to those for variables, with the types pulled out of a global environment – not represented in our rules – rather than of the context. In particular, this presentation completely fixes the universe levels of the arguments. In rule \nameref{infrule:indu-fix}, the type of the fixpoint is checked to be well-formed, and then the body is checked against it. The guard condition, although complex, does not vary between the directed and undirected systems, and we thus do not dwell on it. The formalised version of this rule is complicated by the need to consider mutual (co-)fixpoints, but follows the same pattern.
  
  Last but not least, \nameref{infrule:indu-match} follows the same structure as in \cref{fig:bidir-indu,fig:bidir-indu-other}: first, the type of the scrutinee is inferred, then the predicate is verified to be a type and finally the branches are checked.
  An important point is how much information can be retrieved from the scrutinee $s$. Indeed, the universe levels $\lis{i}$ and the parameters $\lis{p}$ used to build the context in which the predicate $P$ and branches $\lis{t}$ are typed are stored in the match constructor. For cumulative inductive types, this is crucial to retain equivalence between the undirected and bidirectional system, and wrongly building the context from the type inferred for the scrutinee led to the bug we discovered. The idea is that the match construction might need to be typed "higher" than the type of inferred for $s$ to be able to type $P$ and $\lis{t}$. Subsequently, a cumulativity check not appearing in the examples above is needed to ensure that the scrutinee checks against the type constructed using $\lis{i}$ and $\lis{p}$. In contrast with parameters, the inferred indices $\lis{b}$ can safely be used in the return type, but proving this is the most subtle part of the correctness proof.

  
  \subsection{The formalisation}

  Let us now go over the formalisation file by file.

  
  \subparagraph{\href{https://github.com/MevenBertrand/metacoq/blob/itp-artefact/bidirectional/theories/BDEnvironmentTyping.v}{BDEnvironmentTyping.v} \& \href{https://github.com/MevenBertrand/metacoq/blob/itp-artefact/bidirectional/theories/BDTyping.v}{BDTyping.v}}
  The first file refines a few definitions on contexts from \href{https://github.com/MevenBertrand/metacoq/blob/itp-artefact/template-coq/theories/EnvironmentTyping.v}{EnvironmentTyping.v} in order to account for the difference between checking and constrained inference. We expect this to eventually replace the less precise definitions.

  The second contains the definition of the bidirectional type system as a mutually defined inductive type whose main part is \href{https://github.com/MevenBertrand/metacoq/blob/2d631dcd91d2315e5a52fea0fdc27e59c30abd57/bidirectional/theories/BDTyping.v\#L29}{\coqe{infering}}.
  The best way to understand this inductive is probably to compare it with \href{https://github.com/MevenBertrand/metacoq/blob/2d631dcd91d2315e5a52fea0fdc27e59c30abd57/pcuic/theories/PCUICTyping.v\#L209}{\coqe{typing}}, the inductive predicate for undirected typing.

  We then go on to proving by hand a custom induction principle, by first introducing a notion of size of a derivation. This induction principle is not as strong as we might expect, as it does not provide the extra induction hypothesis on context and type that would go with McBride's discipline. We did not try to go and prove such a strong induction principle, as we did not need it. Instead, reflecting the discipline in the choice of the predicates proven by induction was enough. But the main reason was that proving such an induction principle effectively corresponds to an inline proof of validity, a property that required quite an important amount of work to get. We still conjecture that such a strong induction principle should be provable, by reproducing some of the lemmas on the undirected typing, with extra care taken to the size of the obtained typing derivations, so as to be able to use e.g.\ substitutivity of typing together with an induction hypothesis.

  \subparagraph{\href{https://github.com/MevenBertrand/metacoq/blob/itp-artefact/bidirectional/theories/BDToPCUIC.v}{BDToPCUIC.v} \& \href{https://github.com/MevenBertrand/metacoq/blob/itp-artefact/bidirectional/theories/BDFromPCUIC.v}{BDFromPCUIC.v}}
  The next two files prove the equivalence between both type system. Correctness (akin to \cref{thm:corr-ccomega}) is \href{https://github.com/MevenBertrand/metacoq/blob/2d631dcd91d2315e5a52fea0fdc27e59c30abd57/bidirectional/theories/BDToPCUIC.v\#L419}{\coqe{infering_typing}} for inference and the following theorems for the other judgements.
  Completeness (akin to \cref{thm:comp-cumul}) is theorem \href{https://github.com/MevenBertrand/metacoq/blob/2d631dcd91d2315e5a52fea0fdc27e59c30abd57/bidirectional/theories/BDFromPCUIC.v\#L387}{\coqe{typing_infering}}.

  The bulk of both proofs is an induction on typing derivation whose most challenging part is the handling of the case constructor, especially the subtle issues around indices described in \cref{sec:pcuic-indu}. Similarly to \cref{sec:ccomega}, correctness relies on the strong properties of validity and subject reduction to reconstruct missing premises, while completeness mostly requires transitivity of conversion and confluence of reduction.

  \subparagraph{\href{https://github.com/MevenBertrand/metacoq/blob/2d631dcd91d2315e5a52fea0fdc27e59c30abd57/bidirectional/theories/BDUnique.v}{BDUnique.v}} This last file contains the proofs of \cref{prop:unique-inf} – \href{https://github.com/MevenBertrand/metacoq/blob/2d631dcd91d2315e5a52fea0fdc27e59c30abd57/bidirectional/theories/BDUnique.v\#L347}{\coqe{uniqueness_inferred}} – and \cref{prop:princ-types} – \href{https://github.com/MevenBertrand/metacoq/blob/2d631dcd91d2315e5a52fea0fdc27e59c30abd57/bidirectional/theories/BDUnique.v\#L355}{\coqe{principal_type}}. Apart from some lemmas on conversion that were only proved for cumulativity in MetaCoq, the induction itself is quite straightforward thanks to the bidirectional structure.

\section{Beyond PCUIC}
  \label{sec:beyond}

  The use of our bidirectional structure is not limited to CIC or PCUIC. On the contrary, we found it crucial to have such a bidirectional type system when designing a gradual extension to CIC \cite{LennonBertrand2020}, for multiple reasons we try and detail below.
  
  But let us first give a bit of context about this extension. The aim was to adapt the ideas of gradual typing \cite{Siek2015} to CIC. Gradual typing aims at incorporating some level of dynamic typing into a static typing discipline. To do so, a new type constructor $\?$ is introduced to represent dynamic type information. At typing time, this $\?$ should be seen as a wildcard that represents "any type" that is to be treated optimistically. In particular, $\?$ should be considered convertible to any type. Conversion is thus replaced by a new relation, called consistency, that corresponds to this intuition. In effect it behaves somewhat similarly to unification, with each $\?$ corresponding to a unification variable. This means in particular that consistency is \emph{not} transitive, as if it were it would be useless: since any type $T$ is consistent with $\?$, if consistency were transitive any two types would be related.

\subparagraph{Localized computation}

  The free-standing conversion rule \nameref{infrule:pts-undir-conv} is powerful, but sometimes too much.

  This was our first use for the bidirectional structure. Indeed, multiple uses of a consistency in a row would have allowed to change the type of a term to any other arbitrary type by going through $\?$ using two conversion rules in a row. Thus, any term would have been typable! Being able to use the conversion rule unrestricted was too much. Instead, the bidirectional system enforces a more localized use of conversion: only once, at the interface between inference and checking. This restriction was enough to make the conversion rule meaningful again.

  More generally, since the equivalence between the undirected and directed variants relies on the properties listed in \cref{prop:ccomega}, when one of these fails the equivalence is endangered. When one envisons a system where this would be the case, the bidirectional approach might be worth considering, as it could stay viable while its undirected counterpart might not.

\subparagraph{Modes for the conversion rule}

  The observation made in \cref{sec:ccomega-bidir} that the unique \nameref{infrule:pts-undir-conv} rule serves two different roles, which is clarified by the separation between checking and constrained inference, is an important one when toying with computation. Indeed, those two different aspects must be accounted for if one wishes to modify conversion and/or reduction. In particular, modifying the definition of conversion without accounting for the specific role of reduction would make rules for checking and constrained inference come out of sync, bringing trouble down the road.
  
  Taking again the example of \cite{LennonBertrand2020}, the \nameref{infrule:pts-check} is modified by directly replacing conversion with the consistency relation usual in gradual typing. But this is not enough, because constrained inference must be handled as well. This is done by supplementing rule \nameref{infrule:pts-sort-inf} by another rule to treat the case when the inferred type reduces to the wildcard $\?$, that can be used as a type – with some care taken. The same happens for all constrained inference rules.

\subparagraph{Bidirectional elaboration}
  In works such as \cite{Saibi1997,Asperti2012,LennonBertrand2020}, the procedure described is not typing but rather elaboration: the subject of the derivation $t$ is in a kind of source syntax and the aim is not only to inspect $t$, but also to output a corresponding $t'$ in another target syntax. The term $t'$ is a more precise account of term $t$, for instance with solved meta-variables, inserted coercions, and so on. The bidirectional structure readily adapts to those settings, with the extra term $t'$ simply considered as an output of all judgements. As such, McBride's discipline as described in \cref{sec:ccomega-bidir} demands that when, in a context $\Gamma$, the subject $t$ elaborates to $t'$ while inferring type $T$, we should have $\Gamma \vdash t' : T$ – and similarly for all other typing judgements. Having all rules locally preserve this invariant ensures that elaborated terms are always well-typed.

\section{Related work}
  \label{sec:related}

\subsection{Constrained inference}
\label{sec:rel-constrained}

  Traces of constrained inference in diverse seemingly ad-hoc workarounds can be found in various works around typing for CIC, illustrating that this notion, although overlooked, is of interest.
  
  In \cite{Pollack1992}, $\Gamma \vdash t : T$ is used for what we write $\Gamma \vdash t \inferty T$, but another judgment written $\Gamma \vdash t :\geq T$ and denoting type inference followed by reduction is used to effectively inline the two hypothesis of our constrained inference rules. Checking is similarly inlined.

  Saïbi \cite{Saibi1997} describes an elaboration mechanism inserting coercions between types. Those are inserted primarily in checking, when both types are known. However he acknowledges the presence of two special classes to handle the need to cast a term to a sort or a function type without more informations, exactly in the places where we resort to constrained inference rather than checking.

  More recently, Sozeau \cite{Sozeau2007} describes a system where conversion is augmented to handle coercion between subset types. Again, $\Gamma \vdash t : T$ is used for inference, and the other judgments are inlined. Of interest is the fact that reduction is not enough to perform constrained inference, because type head constructors can be hidden by the subset construction: a term of subset type such as $\{f : \nat \to \nat \mid f~0 = 0 \}$ should be usable as a function of type $\nat \to \nat$. An erasure procedure is therefore required on top of reduction to remove subset types in the places where we use constrained inference.

  Abel and Coquand \cite{Abel2008} use a judgement written $\Delta \vdash V \delta \Uparrow \operatorname{Set} \rightsquigarrow i$, where a type $V$ is checked to be well-formed, but with its exact level $i$ free. This corresponds very closely to our use of $\pinferty{\uni}$.

  Traces can also be found in the description of Matita's elaboration algorithm \cite{Asperti2012}. Indeed, the presence of meta-variables on top of coercions makes it even clearer that specific treatment of what we identified as constrained inference is required. The authors introduce a special judgement they call type-level enforcing corresponding to our $\pinferty{\uni}$ judgement. As for $\pinferty{\Pi}$, they have two rules to apply a function, one where its inferred type reduces to a product, corresponding to \nameref{infrule:pts-prod-inf}, and another one to handle the case when the inferred type instead reduces to a meta-variable. As Saïbi, they also need a special case for coercions of terms in function and type position. However, their solution is different. They rely on unification, which is available in their setting, to introduce new meta-variables for the domain and codomain of a product type whenever needed. For $\pinferty{\uni}$ though this solution is not viable, as one would need a kind of universe meta-variable. Instead, they rely on backtracking to test multiple possible universe choices.

  Finally, we have already mentioned \cite{LennonBertrand2020} in \cref{sec:beyond}, where the bidirectional structure is crucial in describing a gradual extension to CIC. In particular, and similarly to what happens with meta-variables in \cite{Asperti2012}, all constrained inference rules are duplicated: there is one rule when the head constructor is the desired one, and a second one to handle the gradual wildcard.

\subsection{Completeness}

  Quite a few articles tackle the problem of bidirectional typing in a setting with an untyped – so called Curry-style – abstraction. This is the case of early work by Coquand \cite{Coquand1996}, the type system of Agda as described in \cite{Norell2007}, the systems considered by Abel in many of his papers \cite{Abel2007,Abel2008,Abel2011,Abel2017}, and much of the work of McBride \cite{McBride2016,McBride2018,McBride2019} on the topic. In such systems, $\lambda$-abstractions can only be checked against a given type, but cannot infer one, so that only terms with no $\beta$-redexes are typable. Norell \cite{Norell2007} argues that such $\beta$-redexes are uncommon in real-life programs, so that being unable to type them is not a strong limitation in practice. To circumvent this problem, McBride also adds the possibility of typing annotations to retain the typability of a term during reduction.
  
  While this approach is adapted to programming languages, where the emphasis is on lightweight syntax, it is not tenable for a proof assistant kernel, where all valid terms should be accepted. Indeed, debugging a proof that is rejected because the kernel fails to accept a perfectly well-typed term the user never wrote – as most proofs are generated rather than written directly – is simply not an option.

  In a setting with typed – Church-style – abstraction, if one wishes to give the possibility for seemingly untyped abstraction, another mechanism has to be resorted to, typically meta-variables. This is what is done in Matita \cite{Asperti2012}, where the authors combine a rule similar to 
  \nameref{infrule:pts-abs} – where the type of an abstraction is inferred – with another one, similar to the Curry-style one – where abstraction is checked – looking like this:
  \begin{mathpar} 
    \inferrule{T \rtred \P x : A' . B \\ \Gamma \vdash A \pinferty{\uni} \uni[i] \\ A \conv A' \\ \Gamma, x : A \vdash t \checkty B}{\Gamma \vdash \l x : A . t \checkty T}
  \end{mathpar}
  While such a rule would make a simple system such as that of \cref{sec:ccomega} “over-complete”, it is a useful addition to enable information from checking to be propagated upwards in the derivation. This is crucial in systems where completeness is lost, such as Matita's elaboration. Similar rules are described in \cite{Asperti2012} for let-bindings and constructors of inductive types.

  Although only few authors consider the problem of a complete bidirectional algorithm for type-checking dependent types, we are not the first to attack it. Already Pollack \cite{Pollack1992} does, and the completeness proof for \CCo{} of \cref{sec:ccomega} is very close to one given in his article. Another proof of completeness for a more complex CIC-like system can be found in \cite{Sozeau2007}. None of those however tackle as we do the whole complexity of PCUIC.
  
\subsection{Inputs and outputs}

  We already credited the discipline we adopt on well-formedness of inputs and outputs to McBride \cite{McBride2018,McBride2019}. A similar idea has also appeared independently in \cite{Bauer2020}. Bauer and his co-authors introduce the notions of a (weakly) presuppositive type theory \cite[Def.~5.6]{Bauer2020} and of well-presented premise-family and rule-boundary \cite[Def.~6.16 and 6.17]{Bauer2020} to describe a discipline similar to ours, using what they call the boundary of a judgment as the equivalent of our inputs and outputs. Due to their setting being undirected, this is however more restrictive, because they are not able to distinguish inputs from outputs and thus cannot relax their condition to only demand inputs to be well-formed but not outputs.

\section{Conclusion}

  We have described a judgmental presentation of the bidirectional structure of typing algorithms in the setting of dependent types. In particular, we identified a new family of judgements we called constrained inference. Those have no counterpart in the non-dependent setting, as they result from a choice of modes for the conversion rule, which is specific to the dependent setting. We proved our bidirectional presentation equivalent to an undirected one, both on paper on the simple case of \CCo{}, and formally in the much more complex and realistic setting of PCUIC. Finally, we gave various arguments for the usefulness of our presentation as a way to ease proofs, an intermediate between undirected type-systems and typing algorithms, a solid basis to design new type systems, and a tool to re-interpret previous work on type systems in a clearer way.

  Regarding future work, a type-checking algorithm is already part of MetaCoq, and we should be able to use our bidirectional type system to give a pleasant completeness proof by separating the concerns pertaining to bidirectionality from the algorithmic problems, such as implementation of an efficient conversion check or proof of termination.
  More broadly, bidirectional type systems should be an interesting tool in the feat of incorporating in proof assistants features that have been satisfactorily investigated on the theoretical level while keeping a complete and correct kernel, avoiding the pitfall of cumulative inductive type's incomplete implementation in Coq.
  A first step would be to investigate the discrepancies between the two kinds of presentations of inductive types \cref{sec:to-pcuic}, and in particular if all informations currently stored in the match node are really needed or if a more concise presentation can be given. But we could go further and study how to handle cubical type theory \cite{Vezzosi2019}, rewrite rules \cite{Cockx2021}, setoid type theory \cite{Altenkirch2019}, exceptional type theory \cite{Pedrot2018}, $\eta$-conversion…
  There might also be an interesting link to make with the current work on normalization by evaluation \cite{Abel2010} as an alternative to weak-head reduction for constrained inference.
  Finally, we hope that our methodology will be adapted as a base for other theoretical investigations. As a way to ease this adoption, studying it in a general setting such as that of \cite{Bauer2020} might be a strong argument for adoption.
%%
%% Bibliography
%%

%% Please use bibtex, 

\bibliography{biblio}

\end{document}

biblio.bib
% Encoding: UTF-8

@Book{Barendregt1985,
  author    = {Barendregt, H.},
  title     = {The Lambda Calculus: Its Syntax and Semantics. Revised Edition.},
  number    = {103},
  publisher = {North Holland},
  series    = {Studies in Logics and the Foundation of Mathematics},
  abstract  = {This book is the lambda-calculus bible. It contains detailed discussions on syntax, semantics and pragmatics along with many theorems and proofs.},
  file      = {Barendregt1985.pdf:Barendregt1985 - The Lambda Calculus_ Its Syntax and Semantics. Revised Edition..pdf:PDF},
  groups    = {Lambda Calculus, meven:5, Computer Science Textbooks},
  year      = {1985},
}

@Book{Barendregt2013,
  author    = {Barendregt, Henk and Dekkers, Wil and Statman, Richard},
  title     = {Lambda Calculus with Types},
  publisher = {Cambridge University Press},
  file      = {Barendregt2013.pdf:Barendregt2013 - Lambda Calculus with Types.pdf:PDF},
  groups    = {Lambda Calculus, meven:5, Computer Science Textbooks},
  year      = {2013},
}

@InProceedings{Boulier2017,
  author      = {Boulier, Simon and P{\'e}drot, Pierre-Marie and Tabareau, Nicolas},
  booktitle   = {{Certified Programs and Proofs (CPP 2017)}},
  title       = {{The next 700 syntactical models of type theory}},
  doi         = {10.1145/3018610.3018620},
  pages       = {182-194},
  url         = {https://hal.inria.fr/hal-01445835},
  address     = {Paris, France},
  file        = {Boulier2017.pdf:Boulier2017 - The Next 700 Syntactical Models of Type Theory.pdf:PDF;:https\://hal.inria.fr/hal-01445835/file/main.pdf:PDF},
  groups      = {meven:3, Syntactical Models},
  hal_id      = {hal-01445835},
  hal_version = {v1},
  keywords    = {Program translation ; Dependent type theory},
  month       = jan,
  year        = {2017},
}

@Article{Castagna2019,
  author  = {Giuseppe Castagna and Victor Lanvin and Tommaso Petrucciani and Jeremy G. Siek},
  title   = {Gradual Typing: a New Perspective},
  note    = {To appear},
  number  = {POPL\,'19},
  volume  = {3, Article 16},
  file    = {Castagna2019.pdf:Castagna2019 - Gradual Typing_ a New Perspective.pdf:PDF},
  groups  = {Gradual Typing, meven:3},
  journal = {Proceedings of the ACM on Programming Languages},
  month   = jan,
  year    = {2019},
}

@Article{Dagand2018,
  author    = {Pierre-{\'E}variste Dagand and Nicolas Tabareau and {\'E}ric Tanter},
  title     = {Foundations of Dependent Interoperability},
  volume    = {28},
  file      = {Dagand2018.pdf:Dagand2018 - Foundations of Dependent Interoperability.pdf:PDF},
  groups    = {Gradual Typing, meven:3, Proof Assistants},
  journal   = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  urldoi    = {http://dx.doi.org/10.1017/S0956796818000011},
  urlpdf    = {http://pleiad.dcc.uchile.cl/papers/2018/dagandAl-jfp2018.pdf},
  users     = {etanter},
  year      = {2018},
}

@InProceedings{Garcia2016,
  author    = {Ronald Garcia and Alison M. Clark and {\'E}ric Tanter},
  booktitle = {Proceedings of the 43rd ACM Symposium on Principles of Programming Languages (POPL 2016)},
  title     = {Abstracting Gradual Typing},
  pages     = {429--442},
  publisher = {ACM Press},
  address   = {St Petersburg, FL, USA},
  file      = {Garcia2016.pdf:Garcia2016 - Abstracting Gradual Typing.pdf:PDF},
  groups    = {Gradual Typing, meven:4},
  month     = jan,
  urldoi    = {http://dx.doi.org/10.1145/2837614.2837670},
  urlpdf    = {http://pleiad.dcc.uchile.cl/papers/2016/garciaAl-popl2016.pdf},
  users     = {etanter},
  year      = {2016},
}

@Article{Geuvers1991,
  author    = {Geuvers, Herman and Nederhof, Mark-Jan},
  title     = {Modular proof of strong normalization for the calculus of constructions},
  doi       = {10.1017/S0956796800020037},
  number    = {2},
  pages     = {155-189},
  volume    = {1},
  abstract  = {Proof of subject reduction of CoC},
  file      = {Geuvers1991.pdf:Geuvers1991 - Modular Proof of Strong Normalization for the Calculus of Constructions.pdf:PDF},
  groups    = {CIC, meven:4, Pure Type Systems, Conversion},
  journal   = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  year      = {1991},
}

@Article{Gilbert2019,
  author              = {Gilbert, Ga{\"e}tan and Cockx, Jesper and Sozeau, Matthieu and Tabareau, Nicolas},
  title               = {Definitional Proof-Irrelevance without K},
  doi                 = {10.1145/329031610.1145/3290316},
  number              = {POPL},
  pages               = {1-28},
  series              = {POPL'19},
  url                 = {https://hal.inria.fr/hal-01859964},
  volume              = {3},
  file                = {Gilbert2019.pdf:Gilbert2019 - Definitional Proof Irrelevance without K.pdf:PDF;:https\://hal.inria.fr/hal-01859964/file/main_popl.pdf:PDF},
  groups              = {meven:2, Proof Assistants},
  hal_id              = {hal-01859964},
  hal_local_reference = {ACL+},
  hal_version         = {v2},
  journal             = {Proceedings of the ACM on Programming Languages},
  month               = jan,
  publisher           = {{ACM}},
  year                = {2019},
}

@InProceedings{Hofmann1996,
  author    = {Martin Hofmann and Thomas Streicher},
  booktitle = {In Venice Festschrift},
  title     = {The Groupoid Interpretation of Type Theory},
  pages     = {83--111},
  publisher = {Oxford University Press},
  file      = {:Hofmann1996 - The Groupoid Interpretation of Type Theory.ps:PostScript},
  groups    = {CIC, HoTT, meven:2, Models of TT},
  year      = {1996},
}

@InProceedings{Lehmann2017,
  author    = {Nico Lehmann and {\'E}ric Tanter},
  booktitle = {Proceedings of the 44th {ACM SIGPLAN-SIGACT} Symposium on Principles of Programming Languages (POPL 2017)},
  title     = {Gradual Refinement Types},
  pages     = {775--788},
  publisher = {ACM Press},
  address   = {Paris, France},
  file      = {Extended Version:Lehmann2017 - Gradual Refinement Types.pdf:PDF;Paper Version:Lehmann2017.pdf:PDF},
  groups    = {Gradual Typing, meven:3},
  month     = jan,
  urldoi    = {http://dx.doi.org/10.1145/3009837.3009856},
  urlpdf    = {http://pleiad.dcc.uchile.cl/papers/2017/lehmannTanter-popl2017.pdf},
  users     = {etanter , nlehmann},
  year      = {2017},
}

@InProceedings{Levy1999,
  author    = {Levy, Paul Blain},
  booktitle = {Typed Lambda Calculi and Applications},
  title     = {Call-by-Push-Value: A Subsuming Paradigm},
  editor    = {Girard, Jean-Yves},
  pages     = {228--243},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {Call-by-push-value is a new paradigm that subsumes the call-by-name and call-by-value paradigms, in the following sense: both operational and denotational semantics for those paradigms can be seen as arising, via translations that we will provide, from similar semantics for call-by-observable.},
  file      = {Levy1999.pdf:Levy1999 - Call by Push Value_ a Subsuming Paradigm.pdf:PDF},
  groups    = {Effects, meven:4},
  year      = {1999},
}

@Book{MacLane2013,
  author    = {Mac Lane, Saunders},
  title     = {Categories for the Working Mathematician},
  publisher = {Springer Science \& Business Media},
  volume    = {5},
  file      = {:MacLane2013 - Categories for the Working Mathematician.pdf:PDF},
  groups    = {Categories, meven:5, Mathematics Textbooks},
  year      = {2013},
}

@Book{MartinLoef1984,
  author    = {Martin-Löf, Per and Sambin, Giovanni},
  title     = {Intuitionistic Type Theory},
  number    = {1},
  publisher = {{Napoli: Bibliopolis}},
  series    = {Studies in Proof Theory},
  file      = {Martin-Loef1984.djvu:MartinLoef1984 - Intuitionistic Type Theory.djvu:Djvu},
  groups    = {CIC, meven:5},
  year      = {1984},
}

@Article{New2019,
  author     = {New, Max S. and Licata, Daniel R. and Ahmed, Amal},
  title      = {Gradual Type Theory},
  doi        = {10.1145/3290328},
  number     = {POPL},
  volume     = {3},
  articleno  = {15},
  file       = {Extended Version:New2019 - Gradual Type Theory.pdf:PDF;Paper Version:New2019.pdf:PDF},
  groups     = {Gradual Typing, meven:2},
  issue_date = {January 2019},
  journal    = {Proceeding of the ACM on Programming Languages},
  keywords   = {call-by-push-value, gradual typing, graduality},
  month      = jan,
  publisher  = {ACM},
  year       = {2019},
}

@Book{Nordstroem1990,
  author    = {Nordström, Bengt and Petersson, Kent and Smith, Jan M.},
  title     = {Programming in Martin-Löf's Type Theory},
  doi       = {10.1016/0167-6423(91)90006-J},
  pages     = {202-203},
  publisher = {Oxford University Press},
  file      = {Nordstroem1990.pdf:Nordstroem1990 - Programming in Martin Löf's Type Theory.pdf:PDF},
  groups    = {CIC, meven:5},
  journal   = {Science of Computer Programming},
  year      = {1990},
}

@Article{Pedrot2019a,
  author     = {P\'{e}drot, Pierre-Marie and Tabareau, Nicolas},
  title      = {The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects},
  doi        = {10.1145/3371126},
  number     = {POPL},
  volume     = {4},
  address    = {New York, NY, USA},
  file       = {Pedrot2019a.pdf:Pedrot2019a - The Fire Triangle_ How to Mix Substitution, Dependent Elimination, and Effects.pdf:PDF},
  groups     = {Effects, CIC, meven:3, Syntactical Models},
  issue_date = {January 2020},
  journal    = {Proceedings of the ACM on Programming Languages},
  month      = dec,
  publisher  = {Association for Computing Machinery},
  year       = {2019},
}

@InProceedings{Pedrot2018,
  author    = {P{\'e}drot, Pierre-Marie and Tabareau, Nicolas},
  booktitle = {ESOP 2018 - 27th European Symposium on Programming},
  title     = {Failure is Not an Option An Exceptional Type Theory},
  doi       = {10.1007/978-3-319-89884-1\_9},
  pages     = {245-271},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {10801},
  address   = {Thessaloniki, Greece},
  file      = {Pedrot2018.pdf:Pedrot2018 - Failure Is Not an Option an Exceptional Type Theory.pdf:PDF},
  groups    = {Effects, CIC, meven:3, Syntactical Models},
  year      = {2018},
}

@InProceedings{Pedrot2017,
  author    = {P{\'e}drot, Pierre-Marie and Tabareau, Nicolas},
  booktitle = {2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  title     = {An Effectful Way to Eliminate Addiction to Dependence},
  doi       = {10.1109/LICS.2017.8005113},
  url       = {https://hal.inria.fr/hal-01441829},
  file      = {EffectfulDependence.pdf:Pedrot2017 - An Effectful Way to Eliminate Addiction to Dependence.pdf:PDF},
  groups    = {Effects, meven:3},
  year      = {2017},
}

@InCollection{PaulinMohring2015,
  author    = {Paulin-Mohring, Christine},
  booktitle = {All about Proofs, Proofs for All},
  title     = {Introduction to the Calculus of Inductive Constructions},
  editor    = {Bruno Woltzenlogel Paleo and David Delahaye},
  publisher = {College Publications},
  series    = {Studies in Logic (Mathematical logic and foundations)},
  volume    = {55},
  file      = {Paulin-Mohring2015.pdf:PaulinMohring2015 - Introduction to the Calculus of Inductive Constructions.pdf:PDF},
  groups    = {CIC, meven:5, Inductive Types},
  keywords  = {Coq proof assistant ; Calculus of Inductive Constructions},
  year      = {2015},
}

@Book{Pierce2002,
  author    = {Benjamin C. Pierce},
  title     = {Types and Programming Languages},
  publisher = {MIT Press},
  series    = {Mit Press},
  file      = {Pierce2002.pdf:Pierce2002 - Types and Programming Languages.pdf:PDF},
  groups    = {meven:5, Computer Science Textbooks},
  year      = {2002},
}

@InProceedings{Siek2006,
  author    = {Jeremy G. Siek and Walid Taha},
  booktitle = {In Scheme and Functional Programming Workshop},
  title     = {Gradual Typing for Functional Languages},
  pages     = {81--92},
  file      = {:Siek2006 - Gradual Typing for Functional Languages.pdf:PDF},
  groups    = {Gradual Typing, meven:3},
  year      = {2006},
}

@InProceedings{Siek2015,
  author    = {Jeremy G. Siek and Michael M. Vitousek and Matteo Cimini and John Tang Boyland},
  booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
  title     = {Refined Criteria for Gradual Typing},
  doi       = {10.4230/LIPIcs.SNAPL.2015.274},
  editor    = {Thomas Ball and Rastislav Bodik and Shriram Krishnamurthi and Benjamin S. Lerner and Greg Morrisett},
  pages     = {274--293},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume    = {32},
  annote    = {Keywords: gradual typing, type systems, semantics, dynamic languages},
  file      = {Siek2015.pdf:Siek2015 - Refined Criteria for Gradual Typing.pdf:PDF},
  groups    = {Gradual Typing, meven:3},
  year      = {2015},
}

@PhdThesis{Siles2010,
  author = {Siles, Vincent},
  title  = {Investigation on the Typing of Equality in Type Systems},
  file   = {Siles2010.pdf:Siles2010 - Investigation on the Typing of Equality in Type Systems.pdf:PDF},
  groups = {CIC, meven:5, Conversion},
  school = {{\'E}cole Polytechnique},
  year   = {2010},
}

@Article{Tabareau2018,
  author              = {Tabareau, Nicolas and Tanter, {\'E}ric and Sozeau, Matthieu},
  title               = {{Equivalences for Free}},
  doi                 = {10.1145/3234615},
  number              = {ICFP},
  pages               = {1-29},
  series              = {ICFP'18},
  url                 = {https://hal.inria.fr/hal-01559073},
  volume              = {2},
  file                = {Tabareau2018.pdf:Tabareau2018 - Equivalences for Free.pdf:PDF;:https\://hal.inria.fr/hal-01559073/file/main_icfp.pdf:PDF},
  groups              = {CIC, HoTT, meven:3},
  hal_id              = {hal-01559073},
  hal_local_reference = {ACL+},
  hal_version         = {v5},
  journal             = {Proceedings of the ACM on Programming Languages},
  keywords            = {Coq ; Type theory ; Homotopy Type Theory ; Parametricity ; Type structures ; Program reasoning},
  month               = sep,
  publisher           = {{ACM}},
  year                = {2018},
}

@InProceedings{Tanter2015,
  author    = {{\'E}ric Tanter and Nicolas Tabareau},
  booktitle = {Proceedings of the 11th {ACM} Dynamic Languages Symposium (DLS 2015)},
  title     = {Gradual Certified Programming in {Coq}},
  pages     = {26--40},
  publisher = {ACM Press},
  address   = {Pittsburgh, PA, USA},
  file      = {Tanter2015.pdf:Tanter2015 - Gradual Certified Programming in Coq.pdf:PDF},
  groups    = {Gradual Typing, meven:4},
  month     = oct,
  urldoi    = {http://dx.doi.org/10.1145/2816707.2816710},
  urlpdf    = {http://pleiad.dcc.uchile.cl/papers/2015/tanterTabareau-dls2015.pdf},
  users     = {etanter},
  year      = {2015},
}

@Article{Toro2019,
  author    = {Toro, Mat\'{\i}as and Labrada, Elizabeth and Tanter, \'{E}ric},
  title     = {Gradual Parametricity, Revisited},
  doi       = {10.1145/3290330},
  number    = {POPL},
  volume    = {3},
  articleno = {17},
  file      = {Extended Version:Toro2019 - Gradual Parametricity, Revisited.pdf:PDF;Paper Version:Toro2019.pdf:PDF},
  groups    = {Gradual Typing, meven:4},
  journal   = {Proceedings of the ACM on Programming Languages},
  keywords  = {Gradual typing, parametricity, polymorphism},
  month     = jan,
  numpages  = {30},
  publisher = {ACM},
  year      = {2019},
}

@Article{Ziliani2017,
  author    = {Ziliani, Beta and Sozeau, Matthieu},
  title     = {A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading},
  doi       = {10.1017/S0956796817000028},
  pages     = {e10},
  volume    = {27},
  file      = {Ziliani2017.pdf:Ziliani2017 - A Comprehensible Guide to a New Unifier for CIC Including Universe Polymorphism and Overloading.pdf:PDF},
  groups    = {meven:3, Proof Assistants},
  journal   = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  year      = {2017},
}

@TechReport{Veldman2000,
  author = {Wim Veldman},
  title  = {{Understanding and Using Brouwer's Continuity Principle}},
  type   = {techreport},
  file   = {Veldman2000.pdf:Veldman2000 - Understanding and Using Brouwer's Continuity Principle.pdf:PDF},
  groups = {Constructivism, meven:3, Intuitionism},
  school = {University of Nijmegen},
  year   = {2000},
}

@Article{Asperti2012,
  author   = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},
  title    = {{A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions}},
  doi      = {10.2168/LMCS-8(1:18)2012},
  volume   = {{Volume 8, Issue 1}},
  file     = {Asperti2012.pdf:Asperti2012 - A Bi Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions.pdf:PDF},
  groups   = {CIC, meven:3, Proof Assistants, Bidirectional Typing},
  journal  = {Logical Methods in Computer Science},
  keywords = {Computer Science - Logic in Computer Science ; Computer Science - Artificial Intelligence ; D.3.1, F.3.0},
  month    = mar,
  year     = {2012},
}

@PhdThesis{SacerdotiCoen2004,
  author = {Claudio {Sacerdoti Coen}},
  title  = {Knowledge Management of Formal Mathematics and Interactive Theorem Proving (Ph.D. Thesis)},
  file   = {SacerdotiCoen2004.ps:SacerdotiCoen2004 - Knowledge Management of Formal Mathematics and Interactive Theorem Proving (Ph.D. Thesis).ps:PostScript},
  groups = {Proof Assistants},
  month  = mar,
  number = {UBLCS-2004-5},
  school = {University of Bologna (Italy). Department of Computer Science},
  year   = {2004},
}

@InProceedings{Garcia2015,
  author    = {Garcia, Ronald and Cimini, Matteo},
  booktitle = {ACM SIGPLAN Notices},
  title     = {Principal Type Schemes for Gradual Programs},
  doi       = {10.1145/2676726.2676992},
  pages     = {303-315},
  file      = {Garcia2015.pdf:Garcia2015 - Principal Type Schemes for Gradual Programs.pdf:PDF},
  groups    = {Gradual Typing, meven:3},
  month     = may,
  year      = {2015},
}

@Article{Eremondi2019,
  author    = {Joseph Eremondi and {\'E}ric Tanter and Ronald Garcia},
  title     = {Approximate Normalization for Gradual Dependent Types},
  number    = {ICFP},
  volume    = {3},
  file      = {:Eremondi2019 - Approximate Normalization for Gradual Dependent Types.pdf:PDF},
  groups    = {Gradual Typing, meven:3, CIC},
  journal   = {Proceedings of the ACM on Programming Languages},
  month     = aug,
  publisher = {ACM Press},
  users     = {etanter},
  year      = {2019},
}

@PhdThesis{Boulier2018,
  author = {Boulier, S.},
  title  = {Extending Type Theory with Syntactical Models},
  file   = {Boulier2018.pdf:Boulier2018 - Extending Type Theory with Syntactical Models.pdf:PDF},
  groups = {CIC, meven:3, Syntactical Models},
  school = {\'Ecole Mines-Telecom Atlantique},
  year   = {2018},
}

@InProceedings{Altenkirch1999,
  author    = {Altenkirch, Thorsten},
  booktitle = {Proceedings - Symposium on Logic in Computer Science},
  title     = {Extensional equality in intensional type theory},
  doi       = {10.1109/LICS.1999.782636},
  isbn      = {0-7695-0158-3},
  pages     = {412-420},
  file      = {Altenkirch1999.pdf:Altenkirch1999 - Extensional Equality in Intensional Type Theory.pdf:PDF},
  groups    = {CIC, meven:3, HoTT, Models of TT},
  month     = feb,
  year      = {1999},
}

@InProceedings{Brady2004,
  author    = {Brady, Edwin and McBride, Conor and McKinna, James},
  booktitle = {Types for Proofs and Programs},
  title     = {Inductive Families Need Not Store Their Indices},
  editor    = {Berardi, Stefano and Coppo, Mario and Damiani, Ferruccio},
  isbn      = {978-3-540-24849-1},
  pages     = {115--129},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {We consider the problem of efficient representation of dependently typed data. In particular, we consider a language TT based on Dybjer's notion of inductive families [10] and reanalyse their general form with a view to optimising the storage associated with their use. We introduce an execution language, ExTT, which allows the commenting out of computationally irrelevant subterms and show how to use properties of elimination rules to elide constructor arguments and tags in ExTT. We further show how some types can be collapsed entirely at run-time. Several examples are given, including a representation of the simply typed $\lambda$-calculus for which our analysis yields an 80{\%} reduction in run-time storage requirements.},
  address   = {Berlin, Heidelberg},
  file      = {Brady2004.pdf:Brady2004 - Inductive Families Need Not Store Their Indices.pdf:PDF},
  groups    = {meven:2, Inductive Types},
  year      = {2004},
}

@Article{Coquand1988,
  author  = {Thierry Coquand and Gérard Huet},
  title   = {The calculus of constructions},
  doi     = {10.1016/0890-5401(88)90005-3},
  issn    = {0890-5401},
  number  = {2},
  pages   = {95-120},
  volume  = {76},
  file    = {Coquand1988.pdf:Coquand1988 - The Calculus of Constructions.pdf:PDF},
  groups  = {CIC, meven:5},
  journal = {Information and Computation},
  year    = {1988},
}

@InProceedings{PaulinMohring1993,
  author    = {C. Paulin-Mohring},
  booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications},
  title     = {{Inductive Definitions in the System {Coq} - Rules and Properties}},
  editor    = {M. Bezem and J.-F. Groote},
  note      = {LIP research report 92-49},
  number    = {664},
  series    = {Lecture Notes in Computer Science},
  file      = {Paulin-Mohring1993.pdf:PaulinMohring1993 - Inductive Definitions in the System Coq Rules and Properties.pdf:PDF},
  groups    = {CIC, meven:5, Inductive Types},
  school    = {LIP-ENS Lyon},
  type      = {research report},
  year      = {1993},
}

@Article{Barendregt1991,
  author  = {Barendregt, Henk},
  title   = {An Introduction to Generalized Type Systems},
  doi     = {10.1017/S0956796800020025},
  pages   = {125-154},
  volume  = {1},
  file    = {Barendregt1991.pdf:Barendregt1991 - An Introduction to Generalized Type Systems.pdf:PDF},
  groups  = {Lambda Calculus, meven:4, Pure Type Systems},
  journal = {Journal of Functional Programming},
  month   = apr,
  year    = {1991},
}

@InProceedings{Pedrot2019,
  author    = {P{\'e}drot, Pierre-Marie and Tabareau, Nicolas and Fehrmann, Hans Jacob and Tanter, {\'E}ric},
  booktitle = {{ICFP 2019 - 24th ACM SIGPLAN International Conference on Functional Programming}},
  title     = {{A Reasonably Exceptional Type Theory}},
  doi       = {10.1145/3341712},
  publisher = {{ACM}},
  address   = {Berlin, Germany},
  file      = {Pedrot2019.pdf:Pedrot2019 - A Reasonably Exceptional Type Theory.pdf:PDF;:https\://hal.inria.fr/hal-02189128/file/icfp19main-p108-p-48a52d2-41764-final.pdf:PDF},
  groups    = {CIC, Effects, meven:3, Syntactical Models},
  month     = aug,
  year      = {2019},
}

@Article{Dybjer2000,
  author  = {Dybjer, Peter},
  title   = {A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory},
  doi     = {10.2307/2586554},
  volume  = {65},
  file    = {Dybjer2000.pdf:Dybjer2000 - A General Formulation of Simultaneous Inductive Recursive Definitions in Type Theory.pdf:PDF},
  groups  = {CIC, meven:2, Inductive Types, Models of TT},
  journal = {Journal of Symbolic Logic},
  month   = jun,
  year    = {2000},
}

@Manual{CDT2019,
  author = {{The Coq Development Team}},
  title  = {The Coq Proof Assistant, version 8.11.0},
  doi    = {10.5281/zenodo.2554024},
  groups = {meven:5, Proof Assistants, Manuals},
  month  = jan,
  year   = {2019},
}

@InProceedings{Anand2018,
  author    = {Anand, Abhishek and Boulier, Simon and Cohen, Cyril and Sozeau, Matthieu and Tabareau, Nicolas},
  booktitle = {{ITP 2018 - 9th Conference on Interactive Theorem Proving}},
  title     = {{Towards Certified Meta-Programming with Typed Template-Coq}},
  doi       = {10.1007/978-3-319-94821-8\_2},
  pages     = {20-39},
  publisher = {{Springer}},
  series    = {LNCS},
  volume    = {10895},
  address   = {Oxford, United Kingdom},
  file      = {Anand2018.pdf:Anand2018 - Towards Certified Meta Programming with Typed Template Coq.pdf:PDF;:https\://hal.archives-ouvertes.fr/hal-01809681/file/paper_39.pdf:PDF},
  groups    = {meven:1, Proof Assistants},
  month     = jul,
  year      = {2018},
}

@InCollection{Dowek2001,
  author    = {Gilles Dowek},
  booktitle = {Handbook of Automated Reasoning},
  title     = {Chapter 16 - Higher-Order Unification and Matching},
  doi       = {10.1016/B978-044450813-3/50018-7},
  editor    = {Alan Robinson and Andrei Voronkov},
  pages     = {1009-1062},
  publisher = {North-Holland},
  series    = {Handbook of Automated Reasoning},
  groups    = {CIC, meven:5},
  year      = {2001},
}

@TechReport{Rossum2014,
  author = {van Rossum, Guido and Lehtosalo, Jukka and Langa, Łukasz},
  title  = {PEP 484 – Type Hints},
  url    = {https://www.python.org/dev/peps/pep-0484/},
  groups = {Gradual Typing, meven:5},
  school = {The Python Software Foundation},
  year   = {2014},
}

@InProceedings{Siek2008,
  author    = {Siek, Jeremy G. and Vachharajani, Manish},
  booktitle = {Proceedings of the 2008 Symposium on Dynamic Languages},
  title     = {Gradual Typing with Unification-based Inference},
  doi       = {10.1145/1408681.1408688},
  series    = {DLS '08},
  file      = {Siek2008.pdf:Siek2008 - Gradual Typing with Unification Based Inference.pdf:PDF},
  groups    = {meven:2, Gradual Typing},
  year      = {2008},
}

@Article{Kaposi2020,
  author   = {Kaposi, Ambrus and Kovács, András},
  title    = {{Signatures and Induction Principles for Higher Inductive-Inductive Types}},
  doi      = {10.23638/LMCS-16(1:10)2020},
  url      = {https://lmcs.episciences.org/6100},
  volume   = {Volume 16, Issue 1},
  groups   = {Inductive Types},
  journal  = {{Logical Methods in Computer Science}},
  keywords = {Computer Science - Logic in Computer Science},
  month    = {2},
  year     = {2020},
}

@InProceedings{Bernardy2011,
  author    = {Bernardy, Jean-Philippe and Lasson, Marc},
  booktitle = {Foundations of Software Science and Computational Structures},
  title     = {Realizability and Parametricity in Pure Type Systems},
  editor    = {Hofmann, Martin},
  pages     = {108--122},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  file      = {Bernardy2011.pdf:Bernardy2011 - Realizability and Parametricity in Pure Type Systems.pdf:PDF},
  groups    = {meven:3, Syntactical Models, Models of TT},
  year      = {2011},
}

@Unpublished{Shulman2018,
  author        = {Michael Shulman},
  title         = {Linear logic for constructive mathematics},
  note          = {Linear logic and Chu construction for constructive mathematics},
  url           = {https://arxiv.org/pdf/1805.07518.pdf},
  archiveprefix = {arXiv},
  eprint        = {1805.07518},
  groups        = {meven:3, Linear Logic, Constructivism},
  primaryclass  = {math.LO},
  year          = {2018},
}

@InProceedings{Altenkirch2019,
  author    = {Altenkirch, Thorsten and Boulier, Simon and Kaposi, Ambrus and Tabareau, Nicolas},
  booktitle = {{MPC 2019 - 13th International Conference on Mathematics of Program Construction}},
  title     = {{Setoid type theory - a syntactic translation}},
  doi       = {10.1007/978-3-030-33636-3\_7},
  URL       = {https://hal.inria.fr/hal-02281225},
  pages     = {155-196},
  publisher = {{Springer}},
  series    = {LNCS},
  volume    = {11825},
  file      = {Altenkirch2019.pdf:Altenkirch2019 - Setoid Type Theory a Syntactic Translation.pdf:PDF;:https\://hal.inria.fr/hal-02281225/file/mpc2019.pdf:PDF},
  groups    = {CIC, HoTT, meven:3, Syntactical Models},
  month     = oct,
  year      = {2019},
}

@Article{Appel1977a,
  author    = {Appel, K. and Haken, W. and Koch, J.},
  title     = {Every planar map is four colorable. Part II: Reducibility},
  doi       = {10.1215/ijm/1256049012},
  number    = {3},
  pages     = {491--567},
  volume    = {21},
  file      = {Appel1977a.pdf:Appel1977a - Every Planar Map Is Four Colorable. Part II_ Reducibility.pdf:PDF},
  fjournal  = {Illinois Journal of Mathematics},
  groups    = {Popularization, meven:4},
  journal   = {Illinois Journal of Mathematics},
  month     = sep,
  publisher = {Duke University Press},
  year      = {1977},
}

@Article{Appel1977,
  author    = {Appel, K. and Haken, W.},
  title     = {Every planar map is four colorable. Part I: Discharging},
  doi       = {10.1215/ijm/1256049011},
  number    = {3},
  pages     = {429--490},
  volume    = {21},
  file      = {Appel1977.pdf:Appel1977 - Every Planar Map Is Four Colorable. Part I_ Discharging.pdf:PDF},
  fjournal  = {Illinois Journal of Mathematics},
  groups    = {Popularization, meven:4},
  journal   = {Illinois Journal of Mathematics},
  month     = sep,
  publisher = {Duke University Press},
  year      = {1977},
}

@Article{Appel1977b,
  author    = {Appel, K. and Haken, W.},
  title     = {Microfiche supplement to “Every planar map is four colorable. Part I and Part II”},
  doi       = {10.1215/ijm/1256049023},
  number    = {3},
  volume    = {21},
  file      = {Appel1977b.pdf:Appel1977b - Microfiche Supplement to “Every Planar Map Is Four Colorable. Part I and Part II”.pdf:PDF},
  fjournal  = {Illinois Journal of Mathematics},
  groups    = {Popularization, meven:4},
  journal   = {Illinois Journal of Mathematics},
  month     = sep,
  publisher = {Duke University Press},
  year      = {1977},
}

@Article{Sozeau2020,
  author    = {Sozeau, Matthieu and Boulier, Simon and Forster, Yannick and Tabareau, Nicolas and Winterhalter, Th{\'e}o},
  title     = {{Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq}},
  doi       = {10.1145/3371076},
  pages     = {1-28},
  file      = {Sozeau2020.pdf:Sozeau2020 - Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq.pdf:PDF},
  groups    = {meven:4, Proof Assistants, CIC},
  journal   = {Proceedings of the ACM on Programming Languages},
  keywords  = {Proof assistants ; Theory of computation ; Type theory ; Certification ; Type checker},
  month     = jan,
  publisher = {{ACM}},
  year      = {2020},
  url       = {https://hal.archives-ouvertes.fr/hal-02380196},
}

@Article{Sozeau2020a,
  author      = {Sozeau, Matthieu and Anand, Abhishek and Boulier, Simon and Cohen, Cyril and Forster, Yannick and Kunze, Fabian and Malecha, Gregory and Tabareau, Nicolas and Winterhalter, Th{\'e}o},
  title       = {{The MetaCoq Project}},
  doi         = {10.1007/s10817-019-09540-0},
  url         = {https://hal.inria.fr/hal-02167423},
  file        = {:https\://hal.inria.fr/hal-02167423/file/The_MetaCoq_Project.pdf:;:https\://hal.inria.fr/hal-02167423/file/The_MetaCoq_Project.pdf:PDF},
  hal_id      = {hal-02167423},
  hal_version = {v1},
  journal     = {{Journal of Automated Reasoning}},
  month       = {2},
  publisher   = {{Springer Verlag}},
  year        = {2020},
}

@InProceedings{Abel2008,
  author    = {Abel, Andreas and Coquand, Thierry and Dybjer, Peter},
  booktitle = {Mathematics of Program Construction},
  title     = {Verifying a Semantic $\beta$$\eta$-Conversion Test for {Martin-L\"of} Type Theory},
  editor    = {Audebaud, Philippe and Paulin-Mohring, Christine},
  isbn      = {978-3-540-70594-9},
  pages     = {29--56},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of Coquand's algorithm for checking the $\beta$$\eta$-equality of such semantic values in a theory with a predicative universe hierarchy and large elimination rules. Although this algorithm does not rely on normalization by evaluation explicitly, we show that similar ideas can be employed for its verification. In particular, our proof uses the new notions of contextual reification and strong semantic equality.},
  address   = {Berlin, Heidelberg},
  file      = {Abel2008.pdf:Abel2008 - Verifying a Semantic $$$$ Conversion Test for Martin Lof Type Theory.pdf:PDF;:Abel2008 Extended - Verifying a Semantic $$$$ Conversion Test for Martin-Lof Type Theory.pdf:PDF},
  groups    = {meven:2, Proof Assistants},
  year      = {2008},
}

@Unpublished{Herbelin2005,
  author = {Hugo Herbelin},
  title  = {Type inference with algebraic universes in the Calculus of Inductive Constructions},
  note   = {Unpublished Manuscript on algebraic universes},
  url    = {https://www.pauillac.inria.fr/~herbelin/articles/univalgcci.pdf},
  file   = {Herbelin2005.pdf:Herbelin2005 - Type Inference with Algebraic Universes in the Calculus of Inductive Constructions.pdf:PDF},
  groups = {CIC, meven:3, Proof Assistants},
  year   = {2005},
}

@InProceedings{Sozeau2014,
  author    = {Sozeau, Matthieu and Tabareau, Nicolas},
  booktitle = {Interactive Theorem Proving},
  doi       = {10.1007/978-3-319-08970-6_32},
  title     = {Universe Polymorphism in {Coq}},
  editor    = {Klein, Gerwin and Gamboa, Ruben},
  isbn      = {978-3-319-08970-6},
  pages     = {499--514},
  publisher = {Springer International Publishing},
  abstract  = {Universes are used in Type Theory to ensure consistency by checking that definitions are well-stratified according to a certain hierarchy. In the case of the Coq proof assistant, based on the predicative Calculus of Inductive Constructions (pCIC), this hierachy is built from an impredicative sort Prop and an infinite number of predicative Typeiuniverses. A cumulativity relation represents the inclusion order of universes in the core theory. Originally, universes were thought to be floating levels, and definitions to implicitely constrain these levels in a consistent manner. This works well for most theories, however the globality of levels and constraints precludes generic constructions on universes that could work at different levels. Universe polymorphism extends this setup by adding local bindings of universes and constraints, supporting generic definitions over universes, reusable at different levels. This provides the same kind of code reuse facilities as ML-style parametric polymorphism. However, the structure and hierarchy of universes is more complex than bare polymorphic type variables. In this paper, we introduce a conservative extension of pCIC supporting universe polymorphism and treating its whole hierarchy. This new design supports typical ambiguity and implicit polymorphic generalization at the same time, keeping it mostly transparent to the user. Benchmarking the implementation as an extension of the Coq proof assistant on real-world examples gives encouraging results.},
  address   = {Cham},
  file      = {Sozeau2014.pdf:Sozeau2014 - Universe Polymorphism in Coq.pdf:PDF},
  groups    = {CIC, meven:3, Proof Assistants},
  year      = {2014},
}

@Book{Rosenblatt1985,
  author    = {Rosenblatt, Murray and Bishop, Errett},
  title     = {Errett Bishop: Reflections on him and his research},
  editor    = {Contemporary mathematics},
  publisher = {Providence, R.I: American Mathematical Society},
  file      = {Rosenblatt1985.djvu:Rosenblatt1985 - Errett Bishop_ Reflections on Him and His Research.djvu:Djvu},
  groups    = {Constructivism, meven:5},
  year      = {1985},
}

@Book{UniFoundationsProgram2013,
  author    = {{The Univalent Foundations Program}},
  title     = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address   = {Institute for Advanced Study},
  file      = {:HoTT book/UniFoundationsProgram2013 - Homotopy Type Theory_ Univalent Foundations of Mathematics.pdf:PDF},
  groups    = {HoTT, meven:5},
  year      = {2013},
}

@Book{Lang2002,
  author     = {Lang, Serge},
  title      = {Algebra},
  doi        = {10.1007/978-1-4613-0041-0},
  isbn       = {9781461265511},
  publisher  = {Springer New York},
  series     = {Graduate Texts in Mathematics},
  volume     = {211},
  collection = {Graduate Texts in Mathematics},
  file       = {Lang2002.pdf:Lang2002 - Algebra.pdf:PDF},
  groups     = {meven:5, Mathematics Textbooks},
  place      = {New York, NY},
  year       = {2002},
}

@Unpublished{Barendregt1984,
  author = {H. E. Barendregt},
  title  = {Introduction to Lambda Calculus},
  note   = {Course Notes},
  file   = {Barendregt1984.pdf:Barendregt1984 - Introduction to Lambda Calculus.pdf:PDF},
  groups = {Lambda Calculus, meven:5, Computer Science Textbooks},
  year   = {1984},
}

@Book{Levy2003,
  author    = {Levy, Paul B.},
  title     = {Call-by-push-value: A Functional/imperative Synthesis},
  publisher = {Springer},
  file      = {Levy2003.pdf:Levy2003 - Call by Push Value_ a Functional_imperative Synthesis.pdf:PDF},
  groups    = {Effects, meven:4},
  year      = {2003},
}

@Book{Perrin1996,
  author     = {Perrin, Daniel},
  title      = {Cours d’algèbre},
  isbn       = {9782729855529},
  publisher  = {Ellipses},
  series     = {CAPES-agrég mathématiques},
  collection = {CAPES-agrég mathématiques},
  file       = {Perrin1996.djvu:Perrin1996 - Cours D’algèbre.djvu:Djvu},
  groups     = {meven:5, Mathematics Textbooks},
  place      = {Paris},
  year       = {1996},
}

@Book{Carton2014,
  author    = {Carton, Olivier},
  title     = {Langages formels: calculabilité et complexité : cours et exercices corrigés : licence 3 \& master, mathématiques \& informatique, agrégation mathématiques},
  isbn      = {9782311014006},
  publisher = {Vuibert},
  file      = {Carton2014.djvu:Carton2014 - Langages Formels_ Calculabilité Et Complexité _ Cours Et Exercices Corrigés _ Licence 3 & Master, Mathématiques & Informatique, Agrégation Mathématiques.djvu:Djvu},
  groups    = {meven:5, Computer Science Textbooks, Logic},
  place     = {Paris},
  year      = {2014},
}

@Book{Riehl2016,
  author     = {Riehl, Emily},
  title      = {Category theory in context},
  isbn       = {9780486809038},
  publisher  = {Dover Publications},
  series     = {Aurora: Dover modern math originals},
  collection = {Aurora: Dover modern math originals},
  file       = {Riehl2016.pdf:Riehl2016 - Category Theory in Context.pdf:PDF},
  groups     = {Categories, meven:5, Category Theory},
  place      = {Mineola, New York},
  year       = {2016},
}

@Book{Bertot2010,
  author       = {Bertot, Yves and Castéran, Pierre},
  title        = {Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions},
  isbn         = {9783642058806},
  publisher    = {Springer},
  series       = {Texts in theoretical computer science},
  abstractnote = {Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory. This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software},
  collection   = {Texts in theoretical computer science},
  file         = {Bertot2010.pdf:Bertot2010 - Interactive Theorem Proving and Program Development_ Coq’Art_ the Calculus of Inductive Constructions.pdf:PDF},
  groups       = {meven:5, Proof Assistants, Computer Science Textbooks},
  place        = {Berlin},
  year         = {2010},
}

@Book{Amadio1998,
  author     = {Amadio, Roberto M. and Curien, P.-L.},
  title      = {Domains and lambda-calculi},
  isbn       = {9780521622776},
  publisher  = {Cambridge University Press},
  series     = {Cambridge tracts in theoretical computer science},
  collection = {Cambridge tracts in theoretical computer science},
  file       = {Amadio1998.pdf:Amadio1998 - Domains and Lambda Calculi.pdf:PDF},
  groups     = {Lambda Calculus, meven:5},
  place      = {Cambridge, U.K. ; New York},
  year       = {1998},
}

@Book{Eiden2009,
  author    = {Eiden, Jean-Denis},
  title     = {Géométrie analytique classique},
  isbn      = {9782916352084},
  publisher = {Calvage \& Mounet},
  file      = {Eiden2009.djvu:Eiden2009 - Géométrie Analytique Classique.djvu:Djvu},
  groups    = {meven:5, Mathematics Textbooks},
  place     = {Paris},
  year      = {2009},
}

@Manual{Sozeau2019,
  author = {Sozeau, M.},
  title  = {Equations 1.2 Reference Manual},
  file   = {:Sozeau2019a - Equations 1.2 Reference Manual.pdf:PDF},
  groups = {meven:4, Proof Assistants, Manuals},
  month  = mar,
  year   = {2019},
}

@Book{Appel1989,
  author     = {Appel, Kenneth I. and Haken, Wolfgang},
  title      = {Every planar map is four colorable},
  isbn       = {9780821851036},
  publisher  = {American Mathematical Society},
  series     = {Contemporary mathematics},
  collection = {Contemporary mathematics},
  file       = {Appel1989.djvu:Appel1989 - Every Planar Map Is Four Colorable.djvu:Djvu},
  groups     = {Popularization, meven:5},
  place      = {Providence, R.I},
  year       = {1989},
}

@Book{Francinou1995,
  author     = {Francinou, Serge and Gianella, Hervé},
  title      = {Exercices de mathématiques pour l’agrégation: algèbre. 1: ...},
  isbn       = {9782225843662},
  publisher  = {Masson},
  series     = {Agrégation de mathématiques},
  collection = {Agrégation de mathématiques},
  file       = {Francinou1995.djvu:Francinou1995 - Exercices De Mathématiques Pour L’agrégation_ Algèbre. 1_ ....djvu:Djvu},
  groups     = {meven:5, Mathematics Textbooks},
  place      = {Paris},
  year       = {1995},
}

@Book{Baader1998,
  author    = {Baader, Franz and Nipkow, Tobias},
  title     = {Term rewriting and all that},
  isbn      = {9780521455206},
  publisher = {Cambridge University Press},
  file      = {Baader1998.djvu:Baader1998 - Term Rewriting and All That.djvu:Djvu},
  groups    = {meven:5, Computer Science Textbooks},
  place     = {Cambridge ; New York},
  year      = {1998},
}

@Book{Girard1989,
  author     = {Girard, Jean-Yves},
  title      = {Proofs and types},
  isbn       = {9780521371810},
  publisher  = {Cambridge University Press},
  series     = {Cambridge tracts in theoretical computer science},
  collection = {Cambridge tracts in theoretical computer science},
  file       = {Girard1989.pdf:Girard1989 - Proofs and Types.pdf:PDF},
  groups     = {meven:5, Computer Science Textbooks, Logic},
  place      = {Cambridge [England] ; New York},
  year       = {1989},
}

@Unpublished{Danos1992,
  author = {Vincent Danos and Roberto {Di Cosmo}},
  title  = {Introduction to Linear Logic},
  note   = {Course Notes, very preliminary version of \cite{LLPrimer97}},
  url    = {http://www.dicosmo.org/CorsoPisa.dvi},
  file   = {Danos1992.pdf:Danos1992 - Introduction to Linear Logic.pdf:PDF},
  groups = {meven:5, Linear Logic},
  month  = jun,
  year   = {1992},
}

@Book{Jacobs2017,
  author     = {Jacobs, Bart},
  title      = {Introduction to coalgebra: towards mathematics of states and observation},
  isbn       = {9781107177895},
  publisher  = {Cambridge University Press},
  series     = {Cambridge tracts in theoretical computer science},
  collection = {Cambridge tracts in theoretical computer science},
  file       = {Jacobs2017.pdf:Jacobs2017 - Introduction to Coalgebra_ Towards Mathematics of States and Observation.pdf:PDF},
  groups     = {meven:5, Category Theory},
  place      = {Cambridge},
  year       = {2017},
}

@Book{Grifone2016,
  author    = {Grifone, Jean},
  title     = {Algèbre linéaire},
  isbn      = {9782364931831},
  publisher = {Éditions Cépaduès},
  file      = {Grifone2016.djvu:Grifone2016 - Algèbre Linéaire.djvu:Djvu},
  groups    = {meven:5, Mathematics Textbooks},
  year      = {2016},
}

@Book{David2003,
  author    = {David, René and Nour, Karim and Raffali, Christophe},
  title     = {Introduction à la Logique : Théorie de la démonstration},
  publisher = {Dunot},
  file      = {David2003.djvu:David2003 - Introduction À La Logique _ Théorie De La Démonstration.djvu:Djvu},
  groups    = {meven:5, Computer Science Textbooks, Logic},
  keywords  = {DNR},
  year      = {2003},
}

@Unpublished{Winskel2005,
  author = {Winskel, Glynn and Pitts, Andrew},
  title  = {Lecture Notes on Denotational Semantics},
  note   = {Lecture Notes},
  file   = {Winskel2005.pdf:Winskel2005 - Lecture Notes on Denotational Semantics.pdf:PDF},
  groups = {meven:5, Computer Science Textbooks},
  year   = {2005},
}

@Book{Soerensen2006,
  author    = {Morten Heine Sørensen and Pawel Urzyczyn},
  title     = {Lectures on the Curry-Howard isomorphism},
  publisher = {Elsevier Science},
  series    = {Studies in Logic and the Foundations of Mathematics},
  volume    = {149},
  file      = {Srensen2006.pdf:Soerensen2006 - Lectures on the Curry Howard Isomorphism.pdf:PDF},
  groups    = {Lambda Calculus, meven:5, Computer Science Textbooks, Pure Type Systems},
  year      = {2006},
}

@Book{Mahboubi2018,
  author = {Assia Mahboubi and Enrico Tassi and Yves Bertot and Georges Gonthier},
  title  = {Mathematical Components},
  file   = {:Mahboubi2018 - Mathematical Components.pdf:PDF},
  groups = {Proof Assistants, Computer Science Textbooks},
  year   = {2018},
}

@Book{Crochemore2007,
  author    = {Crochemore, Maxime and Hancart, Christophe and Lecroq, Thierry},
  title     = {Algorithms on strings},
  publisher = {Cambridge University Press},
  file      = {:Crochemore2007 - Algorithms on Strings.pdf:PDF},
  groups    = {Algorithmics, Computer Science Textbooks},
  year      = {2007},
}

@Book{Gathen2013,
  author    = {Gathen, Joachim von zur and Gerhard, Jürgen},
  title     = {Modern Computer Algebra},
  edition   = {Third edition},
  isbn      = {9781107039032},
  publisher = {Cambridge University Press},
  file      = {:Gathen2013 - Modern Computer Algebra.pdf:PDF},
  groups    = {Algorithmics, Mathematics Textbooks},
  place     = {Cambridge},
  year      = {2013},
}

@Unpublished{Voevodsky2012,
  author = {Vladimir Voevodsky},
  title  = {A universe polymorphic type system},
  file   = {:Voevodsky2012 - A Universe Polymorphic Type System.pdf:PDF},
  groups = {CIC},
  year   = {2012},
}

@PhdThesis{Gilbert2020,
  author = {Gaëtan Gilbert},
  title  = {A type theory with definitional proof-irrelevance},
  file   = {:Gilbert2020 - A Type Theory with Definitional Proof Irrelevance.pdf:PDF},
  groups = {CIC},
  year   = {2020},
}

@Book{Odifreddi1999,
  author    = {Piergiorgio Odifreddi},
  title     = {Classical recursion theory : the theory of functions and sets of natural numbers},
  edition   = {2},
  publisher = {North Holland},
  file      = {:Odifreddi1999 - Classical Recursion Theory _ the Theory of Functions and Sets of Natural Numbers.pdf:PDF},
  groups    = {Computer Science Textbooks},
  year      = {1999},
}

@InBook{Veldman2009,
  author    = {Veldman, Wim},
  booktitle = {Logicism, Intuitionism, and Formalism. Synthese Library (Studies In Epistemology. Logic, Methodology, and Philosophy of Science)},
  title     = {Brouwer’s Approximate Fixed-Point Theorem is Equivalent to Brouwer’s Fan Theorem},
  doi       = {10.1007/978-1-4020-8926-8_14},
  pages     = {277-299},
  file      = {:Veldman2009 - Brouwer’s Approximate Fixed Point Theorem Is Equivalent to Brouwer’s Fan Theorem.pdf:PDF},
  groups    = {Intuitionism, Constructivism},
  month     = jan,
  year      = {2009},
}

@InProceedings{Griffin1989,
  author    = {Griffin, Timothy G.},
  booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  title     = {A Formulae-as-Type Notion of Control},
  doi       = {10.1145/96709.96714},
  isbn      = {0897913434},
  location  = {San Francisco, California, USA},
  pages     = {47–58},
  publisher = {Association for Computing Machinery},
  series    = {POPL ’90},
  address   = {New York, NY, USA},
  file      = {:Griffin1989 - A Formulae As Type Notion of Control.pdf:PDF},
  groups    = {Effects},
  numpages  = {12},
  year      = {1989},
}

@Book{Caldero2017,
  author    = {Philippe Caldero and Jérôme Germoni},
  title     = {Nouvelle Histoires Hédonistes de Groupes et de Géométries. Tome premier.},
  publisher = {Calvage \& Mounet},
  file      = {:Caldero2017 - Nouvelle Histoires Hédonistes De Groupes Et De Géométries. Tome Premier..djvu:Djvu},
  groups    = {Mathematics Textbooks},
  year      = {2017},
}

@Book{Aigner2018,
  author    = {Martin Aigner and Günter Matthias Ziegler},
  title     = {Proofs from The Book},
  edition   = {6},
  publisher = {Springer},
  file      = {:Aigner2018 - Proofs from the Book.pdf:PDF},
  groups    = {Mathematics Textbooks, Popularization},
  year      = {2018},
}

@Book{Nielson1992,
  author    = {Nielson, Hanne Riis and Nielson, Flemming},
  title     = {Semantics with Applications: A Formal Introduction},
  isbn      = {0471929808},
  publisher = {John Wiley & Sons, Inc.},
  file      = {:Nielson1992 - Semantics with Applications_ a Formal Introduction.pdf:PDF},
  groups    = {Semantics of PL, Computer Science Textbooks},
  year      = {1992},
}

@Unpublished{Streicher2004,
  author   = {Thomas Streicher},
  title    = {Introduction to Category Theory and Categorical Logic},
  pubstate = {Lecture Notes},
  file     = {:Streicher2004 - Introduction to Category Theory and Categorical Logic.pdf:PDF},
  groups   = {Category Theory, Computer Science Textbooks},
  year     = {2004},
}

@InBook{Escardo2004,
  author    = {Martín Escardó},
  booktitle = {Electronic Notes in Theoretical Computer Science},
  title     = {Synthetic topology of data types and classical spaces},
  pages     = {21-156},
  publisher = {Elsevier},
  volume    = {87},
  file      = {:Escardo2004 - Synthetic Topology of Data Types and Classical Spaces.pdf:PDF},
  groups    = {Semantics of PL, Topology},
  year      = {2004},
}

@Book{Awodey2010,
  author     = {Awodey, Steve},
  title      = {Category theory},
  edition    = {2},
  isbn       = {9780199587360},
  publisher  = {Oxford University Press},
  series     = {Oxford logic guides},
  collection = {Oxford logic guides},
  file       = {:Awodey2010 - Category Theory.pdf:PDF},
  groups     = {Category Theory, Computer Science Textbooks},
  place      = {Oxford ; New York},
  year       = {2010},
}

@Book{Cormen2009,
  author    = {Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L. and Stein, Clifford},
  title     = {Introduction to algorithms},
  edition   = {3},
  isbn      = {9780262033848},
  publisher = {MIT Press},
  file      = {:Cormen2009 - Introduction to Algorithms.pdf:PDF},
  groups    = {Algorithmics},
  year      = {2009},
}

@Book{MacLane1994,
  author     = {Mac Lane, Saunders and Moerdijk, Ieke},
  title      = {Sheaves in Geometry and Logic: A First Introduction to Topos Theory},
  doi        = {10.1007/978-1-4612-0927-0},
  isbn       = {9780387977102},
  publisher  = {Springer New York},
  series     = {Universitext},
  collection = {Universitext},
  file       = {:MacLane1994 - Sheaves in Geometry and Logic_ a First Introduction to Topos Theory.djvu:Djvu},
  groups     = {Category Theory},
  year       = {1994},
}

@InBook{Hofmann1997,
  author    = {Hofmann, Martin},
  booktitle = {Extensional Constructs in Intensional Type Theory},
  title     = {Syntax and semantics of dependent types},
  doi       = {10.1007/978-1-4471-0963-1_2},
  isbn      = {978-1-4471-0963-1},
  pages     = {13--54},
  publisher = {Springer London},
  abstract  = {In this chapter we fix a particular syntax for a dependently typed calculus and define an abstract notion of model as well as a general interpretation function mapping syntactical objects to entities in a model. This interpretation function is shown to be sound with respect to the syntax.},
  address   = {London},
  file      = {:Hofmann1997 - Syntax and Semantics of Dependent Types.pdf:PDF},
  groups    = {Models of TT},
  year      = {1997},
}

@Article{Coquand1996,
  author   = {Thierry Coquand},
  title    = {An algorithm for type-checking dependent types},
  doi      = {10.1016/0167-6423(95)00021-6},
  issn     = {0167-6423},
  number   = {1},
  volume   = {26},
  abstract = {We present a simple type-checker for a language with dependent types and let expressions, with a simple proof of correctness.},
  file     = {:Coquand1996 - An Algorithm for Type Checking Dependent Types.pdf:PDF},
  groups   = {Bidirectional Typing},
  journal  = {Science of Computer Programming},
  year     = {1996},
}

@Conference{McBride2019,
  author    = {McBride, Conor},
  booktitle = {25th International Conference on Types for Proofs and Programs},
  title     = {Check the Box!},
  groups    = {Bidirectional Typing},
  month     = jun,
  year      = {2019},
}

@Unpublished{McBride2018,
  author = {McBride, Conor},
  title  = {Basics of Bidirectionalism},
  note   = {Blog post},
  url    = {https://pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism/},
  groups = {Bidirectional Typing},
  month  = aug,
  year   = {2018},
}

@Article{Awodey1996,
  author    = {S. Awodey},
  title     = {Structure in Mathematics and Logic: A Categorical Perspective},
  doi       = {10.1093/philmat/4.3.209},
  number    = {3},
  pages     = {209--237},
  volume    = {4},
  file      = {:Awodey1996 - Structure in Mathematics and Logic_ a Categorical Perspective.pdf:PDF},
  groups    = {Category Theory, Logic},
  journal   = {Philosophia Mathematica},
  publisher = {Oxford University Press},
  year      = {1996},
}

@Article{Pierce2000,
  author     = {Pierce, Benjamin C. and Turner, David N.},
  title      = {Local Type Inference},
  doi        = {10.1145/345099.345100},
  issn       = {0164-0925},
  number     = {1},
  pages      = {1–44},
  volume     = {22},
  address    = {New York, NY, USA},
  file       = {:Pierce2000 - Local Type Inference.pdf:PDF},
  groups     = {Bidirectional Typing},
  issue_date = {Jan. 2000},
  journal    = {ACM Transactions on Programming Languages and Systems},
  keywords   = {subtyping, type inference, polymorphism},
  month      = jan,
  numpages   = {44},
  publisher  = {Association for Computing Machinery},
  year       = {2000},
}

@InBook{DeBruijn1991,
  author    = {De Bruijn, N. G.},
  booktitle = {Logical Frameworks},
  title     = {A plea for weaker frameworks},
  doi       = {10.1017/CBO9780511569807.004},
  editor    = {Huet, Gerard and Plotkin, Gordon},
  pages     = {40–68},
  publisher = {Cambridge University Press},
  file      = {:DeBruijn1991 - A Plea for Weaker Frameworks.pdf:PDF},
  groups    = {Proof Assistants},
  place     = {Cambridge},
  year      = {1991},
}

@Article{Abel2012,
  author   = {Abel, Andreas and Scherer, Gabriel},
  title    = {{On Irrelevance and Algorithmic Equality in Predicative Type Theory}},
  doi      = {10.2168/LMCS-8(1:29)2012},
  url      = {https://lmcs.episciences.org/1045},
  volume   = {Volume 8, Issue 1},
  file     = {:Abel2012 - On Irrelevance and Algorithmic Equality in Predicative Type Theory.pdf:PDF},
  journal  = {{Logical Methods in Computer Science}},
  keywords = {Computer Science - Logic in Computer Science ; Computer Science - Programming Languages ; F.4.1},
  month    = {3},
  year     = {2012},
}

@InProceedings{Geuvers2001,
  author    = {Geuvers, Herman},
  booktitle = {Typed Lambda Calculi and Applications},
  title     = {Induction Is Not Derivable in Second Order Dependent Type Theory},
  editor    = {Abramsky, Samson},
  isbn      = {978-3-540-45413-7},
  pages     = {166--181},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  file      = {:Geuvers2001 - Induction Is Not Derivable in Second Order Dependent Type Theory.ps:PostScript},
  groups    = {Inductive Types, Models of TT, Pure Type Systems},
  year      = {2001},
}

@PhdThesis{Sozeau2008,
  author = {Matthieu Sozeau},
  title  = {Un environnement pour la programmation avec types dépendants},
  file   = {:Sozeau2008 - Un Environnement Pour La Programmation Avec Types Dépendants.pdf:PDF},
  groups = {Bidirectional Typing, Proof Assistants},
  school = {Université Paris 11},
  year   = {2008},
}

@Unpublished{Dunfield2019,
  author        = {Jana Dunfield and Neel Krishnaswami},
  title         = {Bidirectional Typing},
  url           = {https://arxiv.org/pdf/1908.05839.pdf},
  archiveprefix = {arXiv},
  eprint        = {1908.05839},
  file          = {:Dunfield2019 - Bidirectional Typing.pdf:PDF},
  groups        = {Bidirectional Typing},
  primaryclass  = {cs.PL},
  year          = {2019},
}

@InProceedings{McBride2016,
  author    = {McBride, Conor},
  booktitle = {A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday},
  title     = {I Got Plenty o' Nuttin'},
  doi       = {10.1007/978-3-319-30936-1_12},
  editor    = {Lindley, Sam and McBride, Conor and Trinder, Phil and Sannella, Don},
  isbn      = {978-3-319-30936-1},
  pages     = {207--233},
  publisher = {Springer International Publishing},
  file      = {:McBride2016 - I Got Plenty O' Nuttin'.pdf:PDF},
  groups    = {Bidirectional Typing, Linear Logic},
  year      = {2016},
}

@InProceedings{Polikarpova2016,
  author    = {Polikarpova, Nadia and Kuraj, Ivan and Solar-Lezama, Armando},
  title     = {Program Synthesis from Polymorphic Refinement Types},
  doi       = {10.1145/2908080.2908093},
  isbn      = {9781450342612},
  pages     = {522–538},
  publisher = {Association for Computing Machinery},
  series    = {PLDI '16},
  address   = {Santa Barbara, CA, USA},
  file      = {:Polikarpova2016 - Program Synthesis from Polymorphic Refinement Types.pdf:PDF},
  groups    = {Bidirectional Typing},
  keywords  = {Predicate Abstraction, Program Synthesis, Functional Programming, Refinement Types},
  numpages  = {17},
  year      = {2016},
}

@Article{Loeh2010,
  author   = {Andres L{\"o}h and Conor Mcbride and Wouter Swierstra},
  title    = {A tutorial implementation of a dependently typed lambda calculus},
  number   = {2},
  pages    = {177--207},
  url      = {https://strathprints.strath.ac.uk/36006/},
  volume   = {102},
  file     = {:Loeh2010 - A Tutorial Implementation of a Dependently Typed Lambda Calculus.pdf:PDF},
  groups   = {Bidirectional Typing, Computer Science Textbooks},
  journal  = {Fundamenta Informaticae},
  keywords = {core calculus, lambda calculus, Haskell, Electronic computers. Computer science, Computational Theory and Mathematics, Algebra and Number Theory, Theoretical Computer Science, Information Systems},
  year     = {2010},
}

@Unpublished{Bauer2020,
  author        = {Andrej Bauer and Philipp G. Haselwarter and Peter LeFanu Lumsdaine},
  title         = {A general definition of dependent type theories},
  note          = {Preprint},
  archiveprefix = {arXiv},
  eprint        = {2009.05539},
  primaryclass  = {math.LO},
  year          = {2020},
}

@Unpublished{Asai2016,
  author = {Asai, Kenichi and Kadowaki, Kyoko},
  title  = {A Type Theoretic Specification of Type Inference},
  file   = {:Asai2016 - A Type Theoretic Specification of Type Inference.pdf:PDF},
  groups = {Bidirectional Typing},
  year   = {2016},
}

@Article{Harper1991,
  author   = {Robert Harper and Robert Pollack},
  title    = {Type checking with universes},
  doi      = {10.1016/0304-3975(90)90108-T},
  issn     = {0304-3975},
  number   = {1},
  url      = {http://www.sciencedirect.com/science/article/pii/030439759090108T},
  volume   = {89},
  abstract = {Various formulations of constructive type theories have been proposed to serve as the basis for machine-assisted proof and as a theoretical basis for studying programming languages. Many of these calculi include a cumulative hierarchy of “universes”, each a type of types closed under a collection of type-forming operations. Universes are of interest for a variety of reasons, some philosophical (predicative vs. impredicative type theories), some theoretical (limitations on the closure properties of type theories) and some practical (to achieve some of the advantages of a type of all types without sacrificing consistency.) The Generalized Calculus of Constructions (CCω) is a formal theory of types that includes such a hierarchy of universes. Although essential to the formalization of constructive mathematics, universes are tedious to use in practice, for one is required to make specific choices of universe levels and to ensure that all choices are consistent. In this paper we study several problems associated with type checking in the presence of universes in the context of CCω. First, we consider the basic type checking and well-typedness problems for this calculus. Second, we consider a formulation of Russell and Whitehead's “typical ambiguity” convention whereby universe levels may be elided, provided that some consistent assignment of levels leads to a correct derivation. Third, we consider the introduction of definitions to both the basic calculus and the calculus with typical ambiguity. This extension leads to a notion of “universe polymorphism” analogous to the type polymorphism of ML. Although our study is conducted for CCω, we expect that our methods will apply to other variants of the Calculus of Constructions and to type theories such as Constable's V3.},
  comment  = {Typical ambiguity},
  file     = {:Harper1991 - Type Checking with Universes.pdf:PDF},
  groups   = {Proof Assistants},
  journal  = {Theoretical Computer Science},
  keywords = {Typical Ambiguity},
  year     = {1991},
}

@Book{Mines1987,
  author    = {Ray Mines and Fred Richman and Wim Ruitenburg},
  title     = {A Course in Constructive Algebra (Universitext)},
  edition   = {1988},
  publisher = {Springer},
  series    = {Universitext},
  file      = {:Mines1987 - A Course in Constructive Algebra (Universitext).djvu:Djvu},
  groups    = {Constructivism, Mathematics Textbooks},
  year      = {1987},
}

@Book{Mines2020,
  author     = {Ray Mines and Fred Richman and Wim Ruitenberg},
  title      = {Un cours d’algèbre constructive},
  publisher  = {Presses Universitaires de Franche-Comté},
  translator = {Henri Lombardi},
  file       = {:Mines2020 - Un Cours D’algèbre Constructive.pdf:PDF},
  groups     = {Constructivism, Mathematics Textbooks},
  month      = feb,
  year       = {2020},
}

@Article{Eilenberg1945,
  author  = {Eilenberg, Samuel and {Mac Lane}, Saunders},
  title   = {General theory of natural equivalences},
  pages   = {231--294},
  volume  = {58},
  file    = {:Eilenberg1945 - General Theory of Natural Equivalences.pdf:PDF},
  groups  = {Category Theory},
  journal = {Transactions of the American Mathematical Society},
  year    = {1945},
}

@Article{Laan1996,
  author    = {Twan Laan and Rob Nederpelt},
  title     = {A Modern Elaboration of the Ramified Theory of Types},
  number    = {2/3},
  pages     = {243--278},
  url       = {http://www.jstor.org/stable/20015876},
  volume    = {57},
  abstract  = {The paper first formalizes the ramified type theory as (informally) described in the Principia Mathematica [32]. This formalization is close to the ideas of the Principia, but also meets contemporary requirements on formality and accuracy, and therefore is a new supply to the known literature on the Principia (like [25], [19], [6] and [7]). As an alternative, notions from the ramified type theory are expressed in a lambda calculus style. This situates the type system of Russell and Whitehead in a modern setting. Both formalizations are inspired by current developments in research on type theory and typed lambda calculus; see [3].},
  file      = {:Laan1996 - A Modern Elaboration of the Ramified Theory of Types.pdf:PDF},
  journal   = {Studia Logica: An International Journal for Symbolic Logic},
  publisher = {Springer},
  year      = {1996},
}

@InProceedings{Pollack1992,
  author    = {R. Pollack},
  booktitle = {Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\aa stad, Sweden},
  title     = {Typechecking in {P}ure {T}ype {S}ystems},
  pages     = {271-288},
  url       = {http://homepages.inf.ed.ac.uk/rpollack/export/BaastadTypechecking.ps.gz},
  file      = {:Pollack1992 - Typechecking in Pure Type Systems.ps:PostScript},
  groups    = {Bidirectional Typing, Pure Type Systems},
  month     = {6},
  year      = {1992},
}

@Unpublished{LennonBertrand2020,
  author        = {Meven Lennon-Bertrand and Kenji Maillard and Nicolas Tabareau and Éric Tanter},
  title         = {Gradualizing the Calculus of Inductive Constructions},
  eprint        = {2011.10618},
  eprinttype    = {arxiv},
  archiveprefix = {arXiv},
  primaryclass  = {cs.PL},
  year          = {2020},
  note          = {Preprint},
}

@InCollection{Barendregt1992,
  author    = {Barendregt, Henk},
  booktitle = {Handbook of Logic in Computer Science},
  title     = {Lambda Calculi with Types},
  publisher = {Oxford Universiy Press},
  file      = {:Barendregt1992 - Lambda Calculi with Types.pdf:PDF},
  groups    = {Pure Type Systems},
  year      = {1992},
}

@InBook{Huet1989,
  author    = {Huet, Gérard},
  booktitle = {A Perspective in Theoretical Computer Science},
  title     = {The Constructive Engine},
  doi       = {10.1142/9789814368452_0004},
  eprint    = {https://www.worldscientific.com/doi/pdf/10.1142/9789814368452_0004},
  pages     = {38-69},
  abstract  = {Abstract The following sections are included: Introduction Technical Preliminaries λ-calculus in the de Bruijn notation Sharing morphisms Binding morphisms with sharing Application to the Calculus of Constructions Term and types Substitution Equality Structure of the environment A digression on the meaning of inference rules Initialization Resetting the current judgement Resetting, pushing and popping the environment Searching the environment The basic machine operations Introducing a new hypothesis Introducing a new definition Global Introduction Prop intro Type intro App intro Discharging definitions Lambda Introduction Product Introduction Type conversion Higher-level commands Sections Inductive definitions The mathematical vernacular A small vernacular syllabus Expressions Commands A full exemple: Newman's lemma Conclusion References},
  file      = {:Huet1989 - The Constructive Engine.pdf:PDF},
  groups    = {Proof Assistants, Bidirectional Typing, Conversion},
  year      = {1989},
}

@InProceedings{Timany2018,
  author    = {Amin Timany and Matthieu Sozeau},
  booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  title     = {{Cumulative Inductive Types In {Coq}}},
  doi       = {10.4230/LIPIcs.FSCD.2018.29},
  editor    = {H{\'e}l{\`e}ne Kirchner},
  isbn      = {978-3-95977-077-4},
  pages     = {1--16},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume    = {108},
  address   = {Dagstuhl, Germany},
  annote    = {Keywords: Coq, Proof Assistants, Inductive Types, Universes, Cumulativity},
  file      = {:Timany2018 - Cumulative Inductive Types in Coq.pdf:PDF},
  groups    = {CIC, Proof Assistants},
  issn      = {1868-8969},
  urn       = {urn:nbn:de:0030-drops-91991},
  year      = {2018},
}

@Article{Saibi1997,
  author  = {Saïbi, Amokrane},
  title   = {Typing Algorithm in Type Theory with Inheritance},
  doi     = {10.1145/263699.263742},
  file    = {:Saibi1997 - Typing Algorithm in Type Theory with Inheritance.pdf:PDF},
  groups  = {Bidirectional Typing, Proof Assistants},
  journal = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’97},
  year    = {1997},
}

@PhdThesis{Norell2007,
  author  = {Ulf Norell},
  title   = {Towards a practical programming language based on dependent type theory},
  address = {SE-412 96 G\"{o}teborg, Sweden},
  file    = {:Norell2007 - Towards a Practical Programming Language Based on Dependent Type Theory.pdf:PDF},
  month   = {9},
  school  = {Department of Computer Science and Engineering, Chalmers University of Technology},
  year    = {2007},
}

@InProceedings{Sozeau2007,
  author    = {Sozeau, Matthieu},
  booktitle = {Types for Proofs and Programs},
  date      = {2007},
  title     = {Subset Coercions in Coq},
  editor    = {Altenkirch, Thorsten and McBride, Conor},
  isbn      = {978-3-540-74464-1},
  doi       = {10.1007/978-3-540-74464-1_16},
  pages     = {237--252},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {We propose a new language for writing programs with dependent types on top of the Coq proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the Coq environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole Coq proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the ``Predicate subtyping'' feature of PVS and following mathematical convention. The typing judgements can be translated to the (CIC) by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the Coq environment.},
  address   = {Berlin, Heidelberg},
  year      = {2007},
}

@InProceedings{Cohen2015,
  author      = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and M{\"o}rtberg, Anders},
  booktitle   = {{21st International Conference on Types for Proofs and Programs}},
  title       = {{Cubical Type Theory: a constructive interpretation of the univalence axiom}},
  doi         = {10.4230/LIPIcs.TYPES.2015.5},
  number      = {69},
  pages       = {262},
  publisher   = {{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}},
  series      = {21st International Conference on Types for Proofs and Programs},
  url         = {https://hal.inria.fr/hal-01378906},
  address     = {Tallinn, Estonia},
  file        = {:https\://arxiv.org/pdf/1611.02108:;:Cohen2015 - Cubical Type Theory_ a Constructive Interpretation of the Univalence Axiom.pdf:PDF;:https\://hal.inria.fr/hal-01378906v2/file/LIPIcs-TYPES-2015-5.pdf:PDF},
  hal_id      = {hal-01378906},
  hal_version = {v2},
  keywords    = {Univalence Axiom ; Dependent Type Theory ; Cubical Sets},
  month       = {5},
  year        = {2015},
}

@Article{Cockx2021,
  author    = {Cockx, Jesper and Tabareau, Nicolas and Winterhalter, Th{\'e}o},
  title     = {{The Taming of the Rew: A Type Theory with Computational Assumptions}},
  series    = {POPL 2021},
  doi       = {10.1145/3434341},
  file      = {:Cockx2021 - The Taming of the Rew_ a Type Theory with Computational Assumptions.pdf:PDF;:https\://hal.archives-ouvertes.fr/hal-02901011v2/file/main_popl.pdf:PDF},
  hal_id    = {hal-02901011},
  journal   = {{Proceedings of the ACM on Programming Languages}},
  keywords  = {type theory ; confluence ; dependent types ; rewriting ; termination},
  publisher = {{ACM}},
  year      = {2021},
}

@Article{Abel2017,
  author     = {Abel, Andreas and \"{O}hman, Joakim and Vezzosi, Andrea},
  title      = {Decidability of Conversion for Type Theory in Type Theory},
  doi        = {10.1145/3158111},
  abstract   = {Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other words, to check whether two types are convertible. We have formalized in Agda a practical conversion checking algorithm for a dependent type theory with one universe \`{a} la Russell, natural numbers, and η-equality for Π types. We prove the algorithm correct via a Kripke logical relation parameterized by a suitable notion of equivalence of terms. We then instantiate the parameterized fundamental lemma twice: once to obtain canonicity and injectivity of type formers, and once again to prove the completeness of the algorithm. Our proof relies on inductive-recursive definitions, but not on the uniqueness of identity proofs. Thus, it is valid in variants of intensional Martin-L\"{o}f Type Theory as long as they support induction-recursion, for instance, Extensional, Observational, or Homotopy Type Theory.},
  address    = {New York, NY, USA},
  articleno  = {23},
  file       = {:Abel2017 - Decidability of Conversion for Type Theory in Type Theory.pdf:PDF},
  issue_date = {January 2018},
  journal    = {Proc. ACM Program. Lang.},
  keywords   = {Agda, Dependent types, Logical relations, Formalization},
  month      = dec,
  numpages   = {29},
  publisher  = {Association for Computing Machinery},
  year       = {2017},
}

@Article{Abel2017a,
  author     = {Abel, Andreas and Vezzosi, Andrea and Winterhalter, Theo},
  title      = {Normalization by Evaluation for Sized Dependent Types},
  doi        = {10.1145/3110277},
  number     = {ICFP},
  volume     = {1},
  abstract   = {Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics. In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier ∀ which lets us ignore sizes in terms for equality checking, alongside with a second quantifier Π for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.},
  address    = {New York, NY, USA},
  articleno  = {33},
  file       = {:Abel2017a - Normalization by Evaluation for Sized Dependent Types.pdf:PDF},
  groups     = {Bidirectional Typing},
  issue_date = {September 2017},
  journal    = {Proc. ACM Program. Lang.},
  keywords   = {universes, proof irrelevance, dependent types, subtyping, normalization-by-evaluation, sized types, eta-equality},
  month      = aug,
  numpages   = {30},
  publisher  = {Association for Computing Machinery},
  year       = {2017},
}

@Article{Vezzosi2019,
  author     = {Vezzosi, Andrea and M\"{o}rtberg, Anders and Abel, Andreas},
  title      = {Cubical {Agda}: A Dependently Typed Programming Language with Univalence and Higher Inductive Types},
  doi        = {10.1145/3341691},
  number     = {ICFP},
  volume     = {3},
  abstract   = {Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.},
  address    = {New York, NY, USA},
  articleno  = {87},
  file       = {:Vezzosi2019 - Cubical Agda_ a Dependently Typed Programming Language with Univalence and Higher Inductive Types.pdf:PDF},
  issue_date = {August 2019},
  journal    = {Proc. ACM Program. Lang.},
  keywords   = {Dependent Pattern Matching, Higher Inductive Types, Cubical Type Theory, Univalence},
  month      = jul,
  numpages   = {29},
  publisher  = {Association for Computing Machinery},
  year       = {2019},
}

@InProceedings{Altenkirch2014,
  author            = {Altenkirch, Thorsten and Li, Nuo and Ondřej, Rypáček},
  title             = {Some constructions on ω-groupoids},
  doi               = {10.1145/2631172.2631176},
  isbn              = {9781450328173},
  organization      = {Vienna, Austria},
  publisher         = {Association for Computing Machinery (ACM)},
  url               = {http://eprints.nottingham.ac.uk/id/eprint/28381},
  abstract          = {Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the construc- tive semantics of Homotopy Type Theory [10]. Following up on our previous formalisation [3] and Brunerie’s notes [5], we present a new formalisation of the syntax of weak ω- groupoids in Agda using heterogeneous equality. We show how to recover basic constructions on ω-groupoids using sus- pension and replacement. In particular we show that any type forms a groupoid and we outline how to derive higher dimensional composition. We present a possible semantics using globular sets and discuss the issues which arise when using globular types instead.},
  conference        = {International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP '14)},
  file              = {:Altenkirch2014 - Some Constructions on Ω Groupoids.pdf:PDF},
  keyword           = {Logic Programming, Groupoids},
  publicationstatus = {Published},
  year              = {2014},
}

@Article{Takahashi1989,
  author   = {Masako Takahashi},
  title    = {Parallel reductions in λ-calculus},
  doi      = {10.1016/S0747-7171(89)80045-8},
  issn     = {0747-7171},
  number   = {2},
  pages    = {113-123},
  url      = {https://www.sciencedirect.com/science/article/pii/S0747717189800458},
  volume   = {7},
  abstract = {The notion of parallel reduction is extracted from the Tait-Martin-Löf proof of the Church-Rosser theorem (for β-reduction). We define parallel β-, η- and βη-reduction by induction, and use them to give simple proofs of some fundamental theorems in λ-calculus; the normal reduction theorem for β-reduction, that for βη-reduction, the postponement theorem of η-reduction (in βη-reduction), and some others.},
  file     = {:Takahashi1989 - Parallel Reductions in Λ Calculus.pdf:PDF},
  groups   = {Conversion},
  journal  = {Journal of Symbolic Computation},
  year     = {1989},
}

@InProceedings{Gonthier2011,
  author    = {Gonthier, Georges},
  booktitle = {Interactive Theorem Proving},
  title     = {Point-Free, Set-Free Concrete Linear Algebra},
  editor    = {van Eekelen, Marko and Geuvers, Herman and Schmaltz, Julien and Wiedijk, Freek},
  isbn      = {978-3-642-22863-6},
  pages     = {103--118},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {Abstract linear algebra lets us reason and compute with collections rather than individual vectors, for example by considering entire subspaces. Its classical presentation involves a menagerie of different settheoretic objects (spaces, families, mappings), whose use often involves tedious and non-constructive pointwise reasoning; this is in stark contrast with the regularity and effectiveness of the matrix computations hiding beneath abstract linear algebra. In this paper we show how a simple variant of Gaussian elimination can be used to model abstract linear algebra directly, using matrices only to represent all categories of objects, with operations such as subspace intersection and sum. We can even provide effective support for direct sums and subalgebras. We have formalized this work in Coq, and used it to develop all of the group representation theory required for the proof of the Odd Order Theorem, including results such as the Jacobson Density Theorem, Clifford's Theorem, the Jordan-Holder Theorem for modules, theWedderburn Structure Theorem for semisimple rings (the basis for character theory).},
  address   = {Berlin, Heidelberg},
  file      = {:Gonthier2011 - Point Free, Set Free Concrete Linear Algebra.pdf:PDF},
  groups    = {Proof Assistants},
  year      = {2011},
}

@InProceedings{Jim1996,
  author    = {Jim, Trevor},
  booktitle = {Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  title     = {What Are Principal Typings and What Are They Good For?},
  doi       = {10.1145/237721.237728},
  isbn      = {0897917693},
  location  = {St. Petersburg Beach, Florida, USA},
  pages     = {42–53},
  publisher = {Association for Computing Machinery},
  series    = {POPL '96},
  abstract  = {We demonstrate the pragmatic value of the principal typing property, a property distinct from ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection types and is closely related to ML. Its principal typing property provides elegant support for separate compilation, including "smartest recompilation" and incremental type inference. Moreover, it motivates a new rule for typing recursive definitions that can type some interesting examples of polymorphic recursion.},
  address   = {New York, NY, USA},
  file      = {:Jim1996 - What Are Principal Typings and What Are They Good For_.pdf:PDF},
  groups    = {Bidirectional Typing},
  numpages  = {12},
  year      = {1996},
}

@Article{McLarty2019,
  author    = {McLarty, Colin},
  title     = {The large structures of Grothendieck founded on finite order arithmetic},
  doi       = {10.1017/s1755020319000340},
  issn      = {1755-0211},
  number    = {2},
  pages     = {296–325},
  volume    = {13},
  groups    = {Logic},
  journal   = {The Review of Symbolic Logic},
  month     = {8},
  publisher = {Cambridge University Press (CUP)},
  year      = {2019},
}

@InProceedings{Gimenez1995,
  author    = {Gim{\'e}nez, Eduarde},
  booktitle = {Types for Proofs and Programs},
  title     = {Codifying guarded definitions with recursive schemes},
  editor    = {Dybjer, Peter and Nordstr{\"o}m, Bengt and Smith, Jan},
  isbn      = {978-3-540-47770-9},
  pages     = {39--59},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {We formalize an extension of the Calculus of Constructions with inductive and coinductive types which allows a more direct description of recursive definitions. The approach we follow is close to the one proposed for Martin-L{\"o}f's type theory in [5]. Recursive objects can be defined by fixed-point definitions as in functional programming languages, and a syntactical checking of these definitions avoids the introduction of non-normalizable terms. We show that the conditions for accepting a recursive definition proposed in [5] are not sufficient for the Calculus of Constructions, and we modify them. As a way of justifying our conditions, we develop a general method to codify a fix point definition satisfying them using well-known recursive schemes, like primitive recursion and co-recursion. We also propose different reduction rules from the ones used in [5] in order to obtain a decidable conversion relation for the system.},
  file      = {:Gimenez1995 - Codifying Guarded Definitions with Recursive Schemes.pdf:PDF},
  groups    = {CIC, Inductive Types, Proof Assistants},
  year      = {1995},
}

@PhdThesis{Cockx2017,
  author   = {Cockx, Jesper},
  date     = {2017},
  title    = {Dependent Pattern Matching and Proof-Relevant Unification},
  abstract = {Dependent type theory is a powerful language for writing functional programs with very precise types. It is used to write not only programs but also mathematical proofs that these programs satisfy certain properties. Because of this, languages based on dependent types – such as Coq, Agda, and Idris – are used both as programming languages and as interactive proof assistants. While dependent types give strong guarantees about your programs and proofs, they also impose equally strong requirements on them. This often makes it harder to write programs in a dependently typed language compared to one with a simpler type system. For this reason certain techniques have been developed, such as dependent pattern matching and specialization by unification. These techniques provide an intuitive way to write programs and proofs in dependently typed languages. Previously, dependent pattern matching had only been shown to work in a limited setting. In particular, it relied on the K axiom – also known as the uniqueness of identity proofs – to remove equations of the form x = x. This axiom is inadmissible in many type theories, particularly in the new and promising branch known as homotopy type theory (HoTT). As a result, programs and proofs in these new theories cannot make use of dependent pattern matching and are as a result much harder to write, modify, and understand. Additionally, the interaction of dependent pattern matching with small but practical features such as eta-equality for record types and postponing of unification constraints was poorly understood, resulting in subtle bugs and inconsistencies. In this thesis, we develop dependent pattern matching and unification in a general setting that does not require the K axiom, both from a theoretical perspective and a practical one. In particular, we present a proof-relevant unification algorithm, where each unification rule produces evidence of its correctness. This evidence guarantees that all unification rules are correct by construction, and also gives a computational characterization to each unification rule. To ensure that these techniques are sound and will stay so in face of future extensions to type theory, we show how to translate them to more basic primitive constructs, i.e. the standard datatype eliminators. During this translation, we pay special attention to the computational content of all constructions involved. This guarantees that the intuitions from regular pattern matching carry over to a dependently typed setting. Based on our work, we implemented a complete overhaul of the algorithm for checking definitions by dependent pattern matching in Agda. Our new implementation fixes a substantial number of issues in the old implementation, and is at the same time less restrictive than the old ad-hoc restrictions. Thus it puts the whole system back on a strong foundation. In addition, our work has already been used as the basis for other implementations of dependent pattern matching, such as the Equations package for Coq and the Lean theorem prover. The work in this thesis eliminates all implicit assumptions introduced to the type theory by pattern matching and unification. In the future, we may also want to integrate new principles with pattern matching, for example the higher inductive types introduced by HoTT. The framework presented in this thesis also provides a solid basis for such extensions to be built on.},
  file     = {:Cockx2017 - Dependent Pattern Matching and Proof Relevant Unification.pdf:PDF},
  year     = {2017},
}

@Article{Coste2001,
  author   = {Michel Coste and Henri Lombardi and Marie-Françoise Roy},
  title    = {Dynamical method in algebra: effective Nullstellensätze},
  doi      = {10.1016/S0168-0072(01)00026-4},
  issn     = {0168-0072},
  number   = {3},
  pages    = {203-256},
  url      = {https://www.sciencedirect.com/science/article/pii/S0168007201000264},
  volume   = {111},
  abstract = {We give a general method for producing various effective Null and Positivstellensätze, and getting new Positivstellensätze in algebraically closed valued fields and ordered groups. These various effective Nullstellensätze produce algebraic identities certifying that some geometric conditions cannot be simultaneously satisfied. We produce also constructive versions of abstract classical results of algebra based on Zorn's lemma in several cases where such constructive version did not exist. For example, the fact that a real field can be totally ordered, or the fact that a field can be embedded in an algebraically closed field. Our results are based on the concepts we develop of dynamical proofs and simultaneous collapse.},
  file     = {:Coste2001 - Dynamical Method in Algebra_ Effective Nullstellensätze.pdf:PDF},
  groups   = {Constructivism},
  journal  = {Annals of Pure and Applied Logic},
  keywords = {Dyamical proof, Constructive algebra, Positivstellensatz},
  year     = {2001},
}

@InProceedings{Goguen2005,
  author    = {Goguen, Healfdene},
  booktitle = {Foundations of Software Science and Computational Structures},
  title     = {Justifying Algorithms for $\beta$$\eta$-Conversion},
  editor    = {Sassone, Vladimiro},
  isbn      = {978-3-540-31982-5},
  pages     = {410--424},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {Deciding the typing judgement of type theories with dependent types such as the Logical Framework relies on deciding the equality judgement for the same theory. Implementing the conversion algorithm for $\beta$$\eta$-equality and justifying this algorithm is therefore an important problem for applications such as proof assistants and modules systems. This article gives a proof of decidability, correctness and completeness of the conversion algorithms for $\beta$$\eta$-equality defined by Coquand [3] and Harper and Pfenning [8] for the Logical Framework, relying on established metatheoretic results for the type theory. Proofs are also given of the same properties for a typed algorithm for conversion for System F, a new result.},
  address   = {Berlin, Heidelberg},
  file      = {:Goguen2005 - Justifying Algorithms for beta eta Conversion.pdf:PDF},
  groups    = {Proof Assistants, Pure Type Systems, Conversion},
  year      = {2005},
}

@InProceedings{Barras2005,
  author    = {Barras, Bruno and Gr{\'e}goire, Benjamin},
  booktitle = {Computer Science Logic},
  title     = {On the Role of Type Decorations in the Calculus of Inductive Constructions},
  editor    = {Ong, Luke},
  isbn      = {978-3-540-31897-2},
  pages     = {151--166},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {In proof systems like Coq [16], proof-checking involves comparing types modulo $\beta$-conversion, which is potentially a time-consuming task. Significant speed-ups are achieved by compiling proof terms, see [9]. Since compilation erases some type information, we have to show that convertibility is preserved by type erasure. This article shows the equivalence of the Calculus of Inductive Constructions (formalism of Coq) and its domain-free version where parameters of inductive types are also erased. It generalizes and strengthens significantly a similar result by Barthe and S{\o}rensen [5] on the class of functional Domain-free Pure Type Systems.},
  address   = {Berlin, Heidelberg},
  file      = {:Barras2005 - On the Role of Type Decorations in the Calculus of Inductive Constructions.pdf:PDF},
  groups    = {Conversion},
  year      = {2005},
}

@Article{Barthe2006,
  author    = {Barthe, Gilles and Coquand, Thierry},
  title     = {Remarks on the equational theory of non-normalizing pure type systems},
  doi       = {10.1017/S0956796803004726},
  number    = {2},
  pages     = {137–155},
  volume    = {16},
  file      = {:Barthe2006 - Remarks on the Equational Theory of Non Normalizing Pure Type Systems.pdf:PDF},
  groups    = {Conversion},
  journal   = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  year      = {2006},
}

@InProceedings{Barthe1997,
  author    = {Barthe, Gilles and S{\O}rensen, Morten Heine},
  booktitle = {Logical Foundations of Computer Science},
  title     = {Domain-free pure type systems},
  editor    = {Adian, Sergei and Nerode, Anil},
  isbn      = {978-3-540-69065-8},
  pages     = {9--20},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {Pure type systems feature domain-specified $\lambda$-abstractions $\lambda$x:A.M. We present a variant of pure type systems, which we call domain-free pure type systems, with domain-free $\lambda$-abstractions $\lambda$x.M. We study the basic properties of domain-free pure type systems and establish their formal relationship with pure type systems.},
  address   = {Berlin, Heidelberg},
  file      = {:Barthe1997 - Domain Free Pure Type Systems.pdf:PDF},
  year      = {1997},
}

@Article{Abel2011,
  author   = {Andreas Abel and Thorsten Altenkirch},
  title    = {A Partial Type Checking Algorithm for Type:Type},
  doi      = {10.1016/j.entcs.2011.02.013},
  issn     = {1571-0661},
  note     = {Proceedings of the Second Workshop on Mathematically Structured Functional Programming (MSFP 2008)},
  number   = {5},
  pages    = {3-17},
  volume   = {229},
  abstract = {We analyze a partial type checking algorithm for the inconsistent domain-free pure type system Type:Type (λ⁎). We show that the algorithm is sound and partially complete using a coinductive specification of algorithmic equality. This entails that the algorithm will only diverge due to the presence of diverging computations, in particular it will terminate for all typeable terms.},
  file     = {:Abel2011 - A Partial Type Checking Algorithm for Type_Type.pdf:PDF},
  groups   = {Bidirectional Typing},
  journal  = {Electronic Notes in Theoretical Computer Science},
  keywords = {Dependent Types, Pure Type Systems, Type Checking, Type:Type},
  year     = {2011},
}

@Article{Abel2007,
  author  = {Andreas Abel and Thierry Coquand},
  title   = {Untyped Algorithmic Equality for {Martin-L\"of's} Logical Framework with Surjective Pairs},
  note    = {{TLCA'05} special issue.},
  number  = {4},
  pages   = {345--395},
  volume  = {77},
  file    = {:Abel2007 - Untyped Algorithmic Equality for Martin Lof's Logical Framework with Surjective Pairs.pdf:PDF},
  groups  = {Bidirectional Typing, Conversion},
  journal = {Fundamenta Informaticae},
  year    = {2007},
}

@Book{Pitts2013,
  author     = {Pitts, Andrew M.},
  title      = {Nominal Sets: Names and Symmetry in Computer Science},
  doi        = {10.1017/CBO9781139084673.003},
  pages      = {1–10},
  publisher  = {Cambridge University Press},
  series     = {Cambridge Tracts in Theoretical Computer Science},
  collection = {Cambridge Tracts in Theoretical Computer Science},
  file       = {:Pitts2013 - Nominal Sets_ Names and Symmetry in Computer Science.pdf:PDF},
  place      = {Cambridge},
  year       = {2013},
}

@InProceedings{Abel2010,
  author    = {Andreas Abel},
  booktitle = {Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings},
  title     = {Towards Normalization by Evaluation for the $\beta\eta$-Calculus of Constructions},
  doi       = {10.1007/978-3-642-12251-4},
  editor    = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
  isbn      = {978-3-642-12250-7},
  pages     = {224--239},
  publisher = {Springer-Verlag},
  series    = {Lecture Notes in Computer Science},
  volume    = {6009},
  file      = {:Abel2010 - Towards Normalization by Evaluation for the $$ Calculus of Constructions.pdf:PDF},
  year      = {2010},
}

@Comment{jabref-meta: databaseType:biblatex;}

@Comment{jabref-meta: grouping:
0 AllEntriesGroup:;
1 StaticGroup:Algorithmics\;0\;0\;0x8a8a8aff\;\;\;;
1 StaticGroup:Bidirectional Typing\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Category Theory\;0\;0\;0x8a8a8aff\;\;\;;
1 StaticGroup:CIC\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Computer Science Textbooks\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Constructivism\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Effects\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Gradual Typing\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:HoTT\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Inductive Types\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Intuitionism\;0\;0\;0x8a8a8aff\;\;\;;
1 StaticGroup:Lambda Calculus\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Linear Logic\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Logic\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Manuals\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Mathematics Textbooks\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Models of TT\;2\;1\;0x8a8a8aff\;\;\;;
2 StaticGroup:Syntactical Models\;2\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Popularization\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Proof Assistants\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Semantics of PL\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Topology\;0\;0\;0x8a8a8aff\;\;\;;
1 StaticGroup:Pure Type Systems\;0\;1\;0x8a8a8aff\;\;\;;
1 StaticGroup:Conversion\;0\;1\;0x8a8a8aff\;\;\;;
}

main.bbl
\begin{thebibliography}{10}

\bibitem{Abel2010}
Andreas Abel.
\newblock Towards normalization by evaluation for the $\beta\eta$-calculus of
  constructions.
\newblock In Matthias Blume, Naoki Kobayashi, and Germ{\'a}n Vidal, editors,
  {\em Functional and Logic Programming, 10th International Symposium, FLOPS
  2010, Sendai, Japan, April 19-21, 2010. Proceedings}, volume 6009 of {\em
  Lecture Notes in Computer Science}, pages 224--239. Springer-Verlag, 2010.
\newblock \href {https://doi.org/10.1007/978-3-642-12251-4}
  {\path{doi:10.1007/978-3-642-12251-4}}.

\bibitem{Abel2011}
Andreas Abel and Thorsten Altenkirch.
\newblock A partial type checking algorithm for type:type.
\newblock {\em Electronic Notes in Theoretical Computer Science}, 229(5):3--17,
  2011.
\newblock Proceedings of the Second Workshop on Mathematically Structured
  Functional Programming (MSFP 2008).
\newblock \href {https://doi.org/10.1016/j.entcs.2011.02.013}
  {\path{doi:10.1016/j.entcs.2011.02.013}}.

\bibitem{Abel2007}
Andreas Abel and Thierry Coquand.
\newblock Untyped algorithmic equality for {Martin-L\"of's} logical framework
  with surjective pairs.
\newblock {\em Fundamenta Informaticae}, 77(4):345--395, 2007.
\newblock {TLCA'05} special issue.

\bibitem{Abel2008}
Andreas Abel, Thierry Coquand, and Peter Dybjer.
\newblock Verifying a semantic $\beta$$\eta$-conversion test for {Martin-L\"of}
  type theory.
\newblock In Philippe Audebaud and Christine Paulin-Mohring, editors, {\em
  Mathematics of Program Construction}, pages 29--56, Berlin, Heidelberg, 2008.
  Springer Berlin Heidelberg.

\bibitem{Abel2017}
Andreas Abel, Joakim \"{O}hman, and Andrea Vezzosi.
\newblock Decidability of conversion for type theory in type theory.
\newblock {\em Proc. ACM Program. Lang.}, December 2017.
\newblock \href {https://doi.org/10.1145/3158111} {\path{doi:10.1145/3158111}}.

\bibitem{Altenkirch2019}
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, and Nicolas Tabareau.
\newblock {Setoid type theory - a syntactic translation}.
\newblock In {\em {MPC 2019 - 13th International Conference on Mathematics of
  Program Construction}}, volume 11825 of {\em LNCS}, pages 155--196.
  {Springer}, October 2019.
\newblock URL: \url{https://hal.inria.fr/hal-02281225}, \href
  {https://doi.org/10.1007/978-3-030-33636-3\_7}
  {\path{doi:10.1007/978-3-030-33636-3\_7}}.

\bibitem{Asperti2012}
Andrea Asperti, Wilmer Ricciotti, Claudio~Sacerdoti Coen, and Enrico Tassi.
\newblock {A Bi-Directional Refinement Algorithm for the Calculus of
  (Co)Inductive Constructions}.
\newblock {\em Logical Methods in Computer Science}, {Volume 8, Issue 1}, March
  2012.
\newblock \href {https://doi.org/10.2168/LMCS-8(1:18)2012}
  {\path{doi:10.2168/LMCS-8(1:18)2012}}.

\bibitem{Barendregt1992}
Henk Barendregt.
\newblock Lambda calculi with types.
\newblock In {\em Handbook of Logic in Computer Science}. Oxford Universiy
  Press, 1992.

\bibitem{Bauer2020}
Andrej Bauer, Philipp~G. Haselwarter, and Peter~LeFanu Lumsdaine.
\newblock A general definition of dependent type theories.
\newblock Preprint, 2020.
\newblock \href {http://arxiv.org/abs/2009.05539} {\path{arXiv:2009.05539}}.

\bibitem{Cockx2021}
Jesper Cockx, Nicolas Tabareau, and Th{\'e}o Winterhalter.
\newblock {The Taming of the Rew: A Type Theory with Computational
  Assumptions}.
\newblock {\em {Proceedings of the ACM on Programming Languages}}, 2021.
\newblock \href {https://doi.org/10.1145/3434341} {\path{doi:10.1145/3434341}}.

\bibitem{Coquand1996}
Thierry Coquand.
\newblock An algorithm for type-checking dependent types.
\newblock {\em Science of Computer Programming}, 26(1), 1996.
\newblock \href {https://doi.org/10.1016/0167-6423(95)00021-6}
  {\path{doi:10.1016/0167-6423(95)00021-6}}.

\bibitem{Jim1996}
Trevor Jim.
\newblock What are principal typings and what are they good for?
\newblock In {\em Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on
  Principles of Programming Languages}, POPL '96, page 42–53, New York, NY,
  USA, 1996. Association for Computing Machinery.
\newblock \href {https://doi.org/10.1145/237721.237728}
  {\path{doi:10.1145/237721.237728}}.

\bibitem{LennonBertrand2020}
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, and Éric Tanter.
\newblock Gradualizing the calculus of inductive constructions.
\newblock Preprint, 2020.
\newblock \href {http://arxiv.org/abs/2011.10618} {\path{arXiv:2011.10618}}.

\bibitem{McBride2016}
Conor McBride.
\newblock I got plenty o' nuttin'.
\newblock In Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella,
  editors, {\em A List of Successes That Can Change the World: Essays Dedicated
  to Philip Wadler on the Occasion of His 60th Birthday}, pages 207--233.
  Springer International Publishing, 2016.
\newblock \href {https://doi.org/10.1007/978-3-319-30936-1_12}
  {\path{doi:10.1007/978-3-319-30936-1_12}}.

\bibitem{McBride2018}
Conor McBride.
\newblock Basics of bidirectionalism.
\newblock Blog post, August 2018.
\newblock URL:
  \url{https://pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism/}.

\bibitem{McBride2019}
Conor McBride.
\newblock Check the box!
\newblock In {\em 25th International Conference on Types for Proofs and
  Programs}, June 2019.

\bibitem{Norell2007}
Ulf Norell.
\newblock {\em Towards a practical programming language based on dependent type
  theory}.
\newblock PhD thesis, Department of Computer Science and Engineering, Chalmers
  University of Technology, SE-412 96 G\"{o}teborg, Sweden, 9 2007.

\bibitem{Pedrot2018}
Pierre-Marie P{\'e}drot and Nicolas Tabareau.
\newblock Failure is not an option an exceptional type theory.
\newblock In {\em ESOP 2018 - 27th European Symposium on Programming}, volume
  10801 of {\em LNCS}, pages 245--271, Thessaloniki, Greece, 2018. Springer.
\newblock \href {https://doi.org/10.1007/978-3-319-89884-1\_9}
  {\path{doi:10.1007/978-3-319-89884-1\_9}}.

\bibitem{Pollack1992}
R.~Pollack.
\newblock Typechecking in {P}ure {T}ype {S}ystems.
\newblock In {\em Informal Proceedings of the 1992 Workshop on Types for Proofs
  and Programs, B\aa stad, Sweden}, pages 271--288, 6 1992.
\newblock URL:
  \url{http://homepages.inf.ed.ac.uk/rpollack/export/BaastadTypechecking.ps.gz}.

\bibitem{Saibi1997}
Amokrane Saïbi.
\newblock Typing algorithm in type theory with inheritance.
\newblock {\em Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on
  Principles of Programming Languages - POPL ’97}, 1997.
\newblock \href {https://doi.org/10.1145/263699.263742}
  {\path{doi:10.1145/263699.263742}}.

\bibitem{Siek2015}
Jeremy~G. Siek, Michael~M. Vitousek, Matteo Cimini, and John~Tang Boyland.
\newblock Refined criteria for gradual typing.
\newblock In Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin~S.
  Lerner, and Greg Morrisett, editors, {\em 1st Summit on Advances in
  Programming Languages (SNAPL 2015)}, volume~32 of {\em Leibniz International
  Proceedings in Informatics (LIPIcs)}, pages 274--293. Schloss
  Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015.
\newblock \href {https://doi.org/10.4230/LIPIcs.SNAPL.2015.274}
  {\path{doi:10.4230/LIPIcs.SNAPL.2015.274}}.

\bibitem{Sozeau2007}
Matthieu Sozeau.
\newblock Subset coercions in coq.
\newblock In Thorsten Altenkirch and Conor McBride, editors, {\em Types for
  Proofs and Programs}, pages 237--252, Berlin, Heidelberg, 2007. Springer
  Berlin Heidelberg.
\newblock \href {https://doi.org/10.1007/978-3-540-74464-1_16}
  {\path{doi:10.1007/978-3-540-74464-1_16}}.

\bibitem{Sozeau2020a}
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster,
  Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Th{\'e}o Winterhalter.
\newblock {The MetaCoq Project}.
\newblock {\em {Journal of Automated Reasoning}}, 2 2020.
\newblock URL: \url{https://hal.inria.fr/hal-02167423}, \href
  {https://doi.org/10.1007/s10817-019-09540-0}
  {\path{doi:10.1007/s10817-019-09540-0}}.

\bibitem{Sozeau2020}
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Th{\'e}o
  Winterhalter.
\newblock {Coq Coq Correct! Verification of Type Checking and Erasure for Coq,
  in Coq}.
\newblock {\em Proceedings of the ACM on Programming Languages}, pages 1--28,
  January 2020.
\newblock URL: \url{https://hal.archives-ouvertes.fr/hal-02380196}, \href
  {https://doi.org/10.1145/3371076} {\path{doi:10.1145/3371076}}.

\bibitem{Sozeau2014}
Matthieu Sozeau and Nicolas Tabareau.
\newblock Universe polymorphism in {Coq}.
\newblock In Gerwin Klein and Ruben Gamboa, editors, {\em Interactive Theorem
  Proving}, pages 499--514, Cham, 2014. Springer International Publishing.
\newblock \href {https://doi.org/10.1007/978-3-319-08970-6_32}
  {\path{doi:10.1007/978-3-319-08970-6_32}}.

\bibitem{UniFoundationsProgram2013}
{The Univalent Foundations Program}.
\newblock {\em Homotopy Type Theory: Univalent Foundations of Mathematics}.
\newblock \url{https://homotopytypetheory.org/book}, Institute for Advanced
  Study, 2013.

\bibitem{Timany2018}
Amin Timany and Matthieu Sozeau.
\newblock {Cumulative Inductive Types In {Coq}}.
\newblock In H{\'e}l{\`e}ne Kirchner, editor, {\em 3rd International Conference
  on Formal Structures for Computation and Deduction (FSCD 2018)}, volume 108
  of {\em Leibniz International Proceedings in Informatics (LIPIcs)}, pages
  1--16, Dagstuhl, Germany, 2018. Schloss Dagstuhl--Leibniz-Zentrum fuer
  Informatik.
\newblock \href {https://doi.org/10.4230/LIPIcs.FSCD.2018.29}
  {\path{doi:10.4230/LIPIcs.FSCD.2018.29}}.

\bibitem{Vezzosi2019}
Andrea Vezzosi, Anders M\"{o}rtberg, and Andreas Abel.
\newblock Cubical {Agda}: A dependently typed programming language with
  univalence and higher inductive types.
\newblock {\em Proc. ACM Program. Lang.}, 3(ICFP), July 2019.
\newblock \href {https://doi.org/10.1145/3341691} {\path{doi:10.1145/3341691}}.

\end{thebibliography}
