Stefan pushed to branch report/tcvi at Stefan / Typer

Commits: 603156f3 by Stefan Monnier at 2018-11-15T22:59:56Z -

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== @@ -239,16 +239,17 @@ is a need to try and better understand what those limits to impredicativity should look like.

Let's disappoint the optimistic reader right away: this paper does not solve -this problem. Instead we consider several existing impredicative systems -which are believed to be consistent, and look at them through the lens of -erasability, arguing that \emph{maybe} the soundness of impredicative -quantification is linked to whether or not it's used in a significant way, -as suggested by Carnap~\cite{Fruchart96}. +this problem. But during the design of our experimental language +Typer~\cite{Monnier19a}, we noticed an interesting property shared by several +existing impredicative systems which are believed to be consistent, that +seemed to link impredicativity and erasability, hinting that \emph{maybe} the +soundness of impredicative quantification is linked to whether or not it's +used in a significant way, as suggested by Carnap~\cite{Fruchart96}.

More specifically, we take those systems and refine them with annotations of -\emph{erasability} (which \citet{Miquel01} calls \emph{implicitness}) very -similar to those used in ICC* and EPTS~\cite{Barras08,MishraLinger08}, and -then show that all places that make use of impredicativity can be annotated +\emph{erasability} (which \citet{Miquel01} calls \emph{implicitness}) like +those used in ICC* and EPTS~\cite{Barras08,MishraLinger08}, and then show +that all places that make use of impredicativity can be annotated as erasable.

Armed with this proverbial hammer, we then look at a few other forms of @@ -266,8 +267,8 @@ The contributions of this work are: fields of inductive types are also erasable. \item A suggestion for how to consistently extend CIC with strong elimination of large inductive types. -\item A proof that the same idea cannot similarly be used to consistently - extend CCω with impredicativity in other universes than the bottom one. +\item A proof that the same idea cannot similarly be used to allow + impredicativity in more than one universe. \item A sketch of a calculus with both inductive types and erasability annotations. While this is straightforward, we do not know of such a system published so far, the closest we found being the one described

===================================== refs.bib ===================================== @@ -37,6 +37,15 @@ year = {2000}, }

+@techreport{Monnier19a, + author = {Stefan Monnier}, + institution = {Université de Montréal - DIRO}, + title = {Typer: {ML} boosted with type theory and {S}cheme}, + year = {2019}, + url = {https://www.iro.umontreal.ca/%5C~%7B%7Dmonnier/typer-overview- + 2019.pdf}, +} + @techreport{Fruchart96, address = {Paris}, author = {Thomas Fruchart and Guiseppe Longo},

View it on GitLab: https://gitlab.com/monnier/typer/commit/603156f372e9c4c564066174161065e05716...