[Git][monnier/typer][report/tcvi] -
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/\~{}monnier/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... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/603156f372e9c4c564066174161065e05716... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Stefan