Stefan pushed to branch report/tcvi at Stefan / Typer

Commits: fd3ca2cb by Stefan Monnier at 2019-11-23T19:45:15Z WIP

- - - - -

2 changed files:

- paper.tex - refs.bib

Changes:

===================================== paper.tex ===================================== @@ -264,8 +264,6 @@ might still enjoy consistency. %% a quick overview of the structure. Should be removed before submission. \newpage \tableofcontents

-\FIXME{Improve structure} - \section{Introduction}

%% General plan: @@ -305,12 +303,12 @@ should look like. Let's disappoint the optimistic reader right away: this paper does not solve this problem. But during the design of our experimental language Typer~\cite{Monnier19}, we noticed an interesting property shared by several -existing impredicative systems which are believed to be consistent, that -seemed to link impredicativity and erasability. Some mathematicians, such -as Carnap~\cite{Fruchart96}, have argued that impredicative quantification -might be acceptable as long as those arguments are not used in what we could -describe as a ``significant'' way, so we investigate here whether -erasability might be such a notion of ``insignificance''. +existing impredicative systems, that seemed to link impredicativity and +erasability. Some mathematicians, such as Carnap~\cite{Fruchart96}, have +argued that impredicative quantification might be acceptable as long as +those arguments are not used in what we could describe as a ``significant'' +way, so in a sense this article investigates here whether erasability might +be such a notion of ``insignificance''.

The two main instances of impredicativity in modern type theory are probably Coq's \kw{Prop} universe, which is designed to be erasable, @@ -322,22 +320,31 @@ impredicativity and erasability, yet it is still unclear to what extent the two belong together nor which particular form of erasability would be the true soulmate or impredicativity.

-Coq and the propositional resizing axiom basically link impredicativity -to the concept of erasure usually called \emph{proof irrelevance}, where an -argument is deemed erasable if its type has at most one inhabitant. In the -following sections, we show an affinity between impredicativity and the -somewhat different notion of erasability found in systems like ICC* and -EPTS~\cite{Barras08,MishraLinger08}, where an argument is deemed erasable if -the function only uses it in type annotations. +Coq and the propositional resizing axiom basically link impredicativity to +the concept of erasure usually called \emph{proof irrelevance}, where an +argument is deemed erasable if its type has at most one inhabitant. +In Section~\ref{sec:prop}, we show a strong affinity between the popular +forms of impredicativity and the somewhat different notion of erasability +found in systems like ICC* and EPTS~\cite{Barras08,MishraLinger08}, where an +argument is deemed erasable if the function only uses it in +type annotations.

More specifically, we take various impredicative systems and refine them with annotations of \emph{erasability}, and then show that all impredicative quantifications can be annotated as erasable.

-Armed with this proverbial hammer, we then look at a few other forms of -impredicativity that are known to break consistency and argue that they look -like nails: by restricting those forms of impredicativity to be erasable we -may be able to recover consistency.%% While there is admittedly ample room in +Armed with this proverbial hammer, we then look at the two main limitations +of impredicative quantification in existing systems: the restriction (which +we call no-SELIT) which disallows strong elimination of large inductive +types in systems like Coq, and the fact that only the bottom universe can be +impredicative. We present how we could maybe replace those somewhat ad-hoc +restrictions with the arguably less ad-hoc restriction that impredicative +quantification is restricted to erasable quantification. + +%% a few other forms of impredicativity that are known to break consistency and +%% argue that they look like nails: by restricting those forms of +%% impredicativity to be erasable we may be able to recover consistency.%% +%% While there is admittedly ample room in %% the margins, in order not to spoil their pleasure, we carefully leave it as %% an exercise for the readers to prove (or disprove) the consistency of some %% of the resulting extensions. @@ -350,16 +357,18 @@ The contributions of this work are: types in the impredicative universe, all arguments to impredicative functions and all \emph{large} fields of inductive types are also erasable. -\item A proposal for how to extend CIC with strong elimination of large - inductive types that might plausibly preserve consistency. -\item A proof that the same idea does not allow impredicativity in more than - one universe. +\item A new calculus ECIC which extends CIC with strong elimination of + large inductive types. +\item A proof that the same idea does not directly make impredicativity in + more than one universe consistent. +\item An new calculus EpCCω with an impredicative universe polymorphism + which allows more powerful forms of impredicativity, such as a Church + encoding with strong elimination. \item As needed for some of the above contributions, we sketch 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 by Bernardo~\citet{Bernardo09}. -%% \item The observation that ICC's stronger conversion rule may not be as -%% strong as it seems. \FIXME{really?} + relatively straightforward, we do not know of such a system published so + far, the closest we found being the one described by + Bernardo~\citet{Bernardo09}. \end{itemize}

\iflongversion @@ -666,7 +675,15 @@ a corresponding well-typed term $\Fforget e$ in $\Fforget S$.%% otherwise the %% and erasable applications, so to show that they are related would require %% using x_R in the final result type!?

-\section{Erasing impredicative arguments of CCω} +\section{Erasable impredicativity in \kw{Prop}} +\label{sec:prop} + +In this section we show that the impredicative quantification in the bottom +universe \kw{Prop} is almost always erasable and armed with this observation +along with some circumstantial evidence, we propose to rely on this property +in order to lift the no-SELIT restriction. + +\subsection{Erasing impredicative arguments of CCω}

\FIXME{Abel mentions in~\cite{Abel13} that in the pure CoC, dependent arguments are always erasable, but that this doesn't hold any more @@ -784,7 +801,7 @@ This shows that the erasability of System-F's impredicative type abstractions can be extended to all of CCω's impredicative abstractions as well.

-\section{Erasing impredicative arguments of CIC} +\subsection{Erasing impredicative arguments of CIC} \label{sec:cic}

\newcommand \Ind[3] {\kw{Ind}(#1:#2)\langle#3\rangle} @@ -931,10 +948,10 @@ Two important details are worth pointing out: to be in \kw{Prop}: just like in the original CIC we only allow inductive types in our bottom universe, contrary to what systems like Coq~\cite{Coq00} and UTT~\cite{Luo92} allow. -\item In the \kw{Case} rule we have the condition that when the - result of the case analysis is not in \kw{Prop}, i.e.~when this is a form - of strong elimination, the inductive type must be small, meaning that all - its fields must be in \kw{Prop}. This restriction is taken from +\item In the \kw{Case} rule we have the condition that when the result of + the case analysis is not in \kw{Prop}, i.e.~when this is a form of strong + elimination, the inductive type must be small, meaning that all its fields + must be in \kw{Prop}. This ``no-SELIT'' restriction is taken from \citet{Werner94}, with a slightly different presentation because he splits the \kw{Case} rule into two: one for weak elimination and one for strong elimination. @@ -1015,7 +1032,7 @@ abstractions can be extended not only to all of CCω's impredicative abstractions but also to CIC's impredicative abstractions and impredicative inductive types.

-\section{Strong elimination of large inductive types} +\subsection{Strong elimination of large inductive types}

The reason behind the $\Jsmall e$ special constraint on strong eliminations of CIC in Figure~\ref{fig:cic} is pretty @@ -1038,9 +1055,9 @@ universes. This was first shown to be inconsistent in \cite{Coquand86b}.

This restriction makes the system more complex since elimination is allowed from any inductive type to any universe except for the one special case of -strong elimination of large inductive types. It also significantly weakens -the system. For example while we can define in Coq a large inductive type -like: +strong elimination of large inductive types (SELIT). It also significantly +weakens the system. For example while we can define in Coq a large +inductive type like: \begin{verbatim} Inductive Ω : Set := | int : Ω @@ -1050,8 +1067,8 @@ like: we cannot prove properties such as the following (which we needed while working on~\cite{Monnier07}): \begin{verbatim} - forall K₁ K₂ F₁ F₂ P, - all K₁ F₁ = all K₂ F₂ -> P K₁ F₁ -> P K₂ F₂. + forall k₁ k₂ f₁ f₂ p, + all k₁ f₁ = all k₂ f₂ -> p k₁ f₁ -> p k₂ f₂. \end{verbatim} In practice, this important restriction significantly reduces the applicability of large inductive types. @@ -1093,8 +1110,8 @@ applicability of large inductive types. While the $\Jsmall e$ constraint was added to avoid an inconsistency, this same $\Jsmall e$ is also the key to making our proof of erasability of impredicative arguments work for CIC: it is the detail which makes it -possible to erase all the large fields of impredicative inductive -definitions, as we saw in the previous section. +possible to mark all the large fields of impredicative inductive +definitions as erasable, as we saw in the previous section. This might be a coincidence, of course, yet it suggests a close alignment between the needs of consistency and the need to keep impredicative elements erasable. @@ -1105,9 +1122,9 @@ ECIC is more elegant and regular than CIC thanks to the absence of this special corner case, and it allows typing more terms than \kw{e}CIC and hence CIC. For instance in ECIC we can define the above $\Omega$ inductive type with an erasable $k$ and then prove the mentioned property (again with erasable -$K_1$ and $K_2$). +$k_1$ and $k_2$).

-Note also that the lack of a $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule, +Note also that the lack of an $(\kw{n},\Type{\ell},\kw{Prop},\kw{Prop})$ rule, means we cannot define a \texttt{box} as above in this system; instead we are limited to making its content erasable. This in turn prevents us from defining \texttt{unbox} since the \texttt{x'} would now be erasable so it @@ -1120,7 +1137,7 @@ circumstantial evidence, we venture to state the following: The ECIC system is consistent. \end{conjecture}

-\section{Non-erasable impredicativity in Coq and UTT} +\subsection{Erasing impredicativity in Coq and UTT}

As noted in Section~\ref{sec:cic}, we were careful to restrict our inductive types to live in \kw{Prop}. This was no accident: we can see in the proof @@ -1218,15 +1235,22 @@ Whether the use of thinning is sufficient to show that any valid typing derivation in a system like UTT has a corresponding typing derivation in eCoq is left for future work.

-\section{Multiple levels of impredicativity} +\section{Universe-agnostic impredicativity} + +Like all known consistent type systems that support impredicative +definitions, CCω accepts them only in the bottom universe, called \kw{Prop}. +This is a direct consequence of various paradoxes formalized in systems +which allow impredicative definitions in more than one universe, such as +those shown in \citet{Girard72}, \citet{Coquand94}, and \citet{Hurkens95}. + +In this section we investigate the use of an erasability constraint in order +to lift this restriction and thus allow impredicative definitions in higher +universes as well.

-Like all known consistent systems that support impredicative -definitions, CCω accepts them only in the bottom universe. This is a direct -consequence of various paradoxes formalized -in systems which allow impredicative definitions in more than one universe, -such as those shown in \citet{Girard72}, \citet{Coquand94}, and -\citet{Hurkens95}. The last two showed a paradox in the system $\lambda U^-$ -which can be defined as an EPTS as follows: +\subsection{Erasing impredicative arguments in $\lambda U^-$} + +The last two showed a paradox in the system $\lambda U^-$ which is System-F$_\omega$ +extended with one extra rule. It can be defined as an EPTS as follows: \begin{displaymath} \begin{array}{lcl} \mathcal{S} &=& {~ *,~\square,~\mathrm{\Delta} ~} \ @@ -1335,11 +1359,11 @@ this is not the case: impredicative functions. %% \qed \end{proof}

-This demonstrates that, even though the notion of erasability we use here has -shown strong affinities with consistent uses of impredicativity, it is +This demonstrates that, even though the notion of erasability we use here +has shown strong affinities with consistent uses of impredicativity, it is not in general sufficient to tame the excesses of impredicativity.

-\section{Universe polymorphism} +\subsection{Inductive types: Impredicative and universe polymorphic?}

\FIXME{ Look at Nuyts's work on parametricity and impredicativity @@ -1464,7 +1488,7 @@ the universe level parameter $\ell$ needs to be erasable. k \in {\kw{n},\kw{e}}, \ell \in\mathbb{N}, \ell_2\in\mathbb{N}\cup{\omega} ~} \end{array} \end{displaymath} - \caption{Informal rules of EAgda} + \caption{Informal rules of EpCCω} \label{fig:eagda} \end{figure}

@@ -1497,20 +1521,21 @@ While this places \id{NatL} in $\Type{1}$ rather than $\Type{0}$, it still makes it impredicative, and if all our base types live in $\Type{1}$ we will not notice much difference.

-Figure~\ref{fig:eagda} describes the the resulting calculus EAgda, where the -second fields of elements of $\mathcal{R}$ now have the shape ``$x:s$'' so we -can refer to the variable $x$ that can appear freely in the third field. +Figure~\ref{fig:eagda} describes the resulting calculus we call EpCCω, +where the second fields of elements of $\mathcal{R}$ now have the shape +``$x:s$'' so we can refer to the variable $x$ that can appear freely in the +third field.

-\subsection{The power of EAgda} +\subsection{Encoding System-F in EpCCω}

-EAgda is basically a predicative calculus of constructions, with a tower of +EpCCω is basically a predicative calculus of constructions, with a tower of universes, plus universe polymorphism, plus impredicative erasable universe polymorphism. Compared to Agda, it lacks inductive types but it adds a form of impredicativity. While we do not know if it is consistent, we can try and compare it to existing systems.

\begin{theorem} - EAgda can encode System-F. + EpCCω can encode System-F. \end{theorem} \begin{proof} We take as input a stratified version of System-F, so @@ -1524,11 +1549,11 @@ can try and compare it to existing systems. %% ~|~ \lambda t:\kappa.\tau ~|~ \tau_1~\tau_2 ~|~ \lambda x:\tau_1.\tau_2 ~|~ \tau~e \ \textsl{(terms)} & e &::=& - x ~|~ \lambda x:\tau.e ~|~ e_1~e_2 ~|~ \lambda t:*.e ~|~ e~\tau + x ~|~ \lambda x:\tau \to e ~|~ e_1~e_2 ~|~ \lambda t:* \to e ~|~ e~\tau \end{array} \end{displaymath} \newcommand\Ftoa{\MetaFunction{}} - Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F to EAgda: + Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F to EpCCω: %% FIXME: %% What about Λt₁.Λt₂.id[t₁→t₂→t₁](λx:t₁→λy:t₂→x) ? %% That should turn into @@ -1540,7 +1565,7 @@ can try and compare it to existing systems. \begin{array}{r@{~=~}ll} \MetaFunction{}{\bullet} & \bullet~;~\bullet \ \MetaFunction{}{\Gamma,x:\tau} & - \Gamma',x:\MetaFunction{}{\tau} ~;~ \Delta& + \Gamma',x:\MetaFunction{\Delta}{\tau} ~;~ \Delta& \text{where }\Gamma';\Delta = \MetaFunction{}{\Gamma}\ %% \MetaFunction{s}{\Gamma,t:\kappa} & %% \MetaFunction{s}{\Gamma},t:\MetaFunction{s}{\kappa} \ @@ -1562,12 +1587,12 @@ can try and compare it to existing systems. \text{ and } \ell' = \Tlub{1!!}{!!\Subst{\ell}{0}{l}} \medskip \ \MetaFunction{\Delta}{x} & x \ - \MetaFunction{\Delta}{\lambda x:\tau . e} & + \MetaFunction{\Delta}{\lambda x:\tau \to e} & \Lam[n]{t}{\tau'}{\MetaFunction{\Delta}{e}} & \text{where }\tau';\ell = \MetaFunction{\Delta}{\tau} \ \MetaFunction{\Delta}{e_1~e_2} & \App[n]{\MetaFunction{\Delta}{e_1}}{\MetaFunction{\Delta}{e_2}} \ - \MetaFunction{\Delta}{\lambda t:*.e} & + \MetaFunction{\Delta}{\lambda t:* \to e} & \Lam[e]{l}{\kw{Level}}{ \Lam[n]{t}{\Type{l}}{ \MetaFunction{\Delta,t:l}{e}}} \ @@ -1578,7 +1603,7 @@ can try and compare it to existing systems. \medskip \ %% \MetaFunction{s}{(t:\kappa_1)\to\kappa_2} & %% \Arw[n]{t}{\MetaFunction{s}{\kappa_1}}{\MetaFunction{s}{\kappa_2}} \ - %% \MetaFunction{s}{\lambda t:\kappa . \tau} & + %% \MetaFunction{s}{\lambda t:\kappa \to \tau} & %% \Lam[n]{t}{\MetaFunction{s}{\kappa}}{\MetaFunction{s}{\tau}} \ %% \MetaFunction{s}{\tau_1~\tau_2} & %% \App[n]{\MetaFunction{s}{\tau_1}}{\MetaFunction{s}{\tau_2}} \ @@ -1586,11 +1611,144 @@ can try and compare it to existing systems. \end{array} \end{displaymath} And then we can show by structural induction on the type derivation that - for any $\Jtype{e}{\tau}$ in System-F, we have - $\Jtype[\Gamma']{e'}{\tau'}$ in EAgda where $\Gamma';\Delta = \MetaFunction{}{\Gamma}$, + for any $\Jtype{e}{\tau}$ in System-F, we have $\Jtype[\Gamma']{e'}{\tau'}$ and + $\Jtype[\Gamma']{\tau'}{\Type{\ell}}$ in EpCCω where $\Gamma';\Delta = \MetaFunction{}{\Gamma}$, $e' = \MetaFunction{\Delta}{e}$, and $\tau';\ell = \MetaFunction{\Delta}{\tau}$. \end{proof}

+\subsection{The power of EpCCω} + +EpCCω is flexible enough to cover the kind of impredicativity found in +Church's encoding or in Chlipala's parametric higher-order abstract +syntax~\cite{Chlipala08}. It does it without restricting impredicativity to +a single universe, and moreover those encodings are more flexible in EpCCω +since as we have seen they support the equivalent of strong elimination. +So in this sense EpCCω is more powerful than systems like CCω. + +Yet we have not been able to generalize the above System-F encoding to +encode System-F$_ω$ into EpCCω. For example, consider the following term: +\begin{displaymath} + λt:* \to \lambda (f : *\to*) \to \lambda (x : f~t) \to x +\end{displaymath} +The first two $\lambda$s should be impredicative, so the encoding should +presumably look like: +\begin{displaymath} + \Lam[e]{l_1}{\kw{Level}}{ + \Lam[n]{t}{\Type{l_1}}{ + \Lam[e]{l_2}{\kw{Level}}{ + \Lam[n]{f}{T_1}{ + \Lam[n]{x}{T_2}{ + x}}}}} +\end{displaymath} +We can then choose $T_1$ and $T_2$ as follows: +\begin{displaymath} + \begin{array}{l@{~=~}l} + T_1 & \Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_2}}} \ + T_2 & \App[n]{\App[e]{f}{l_1}}{t} + \end{array} +\end{displaymath} +This makes the term valid, but its semantics doesn't match that of the +original System-F$_\omega$ term since we cannot pass the identity function +$\lambda{}t:*\to{}t$ as $f$ any more: its encoding would now have type +$\Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_3}}}$ instead of +the expected $\Arw[e]{l_3}{\kw{Level}}{\ArwS[n]{\Type{l_3}}{\Type{l_2}}}$. + +Similarly, we have not been able to adapt Hurkens's paradox to the EpCCω +system either. Of course, all this says is that we do not know if EpCCω is +consistent, but it seems to indicate that this kind of impredicativity is +incomparable to the traditional form seen in CCω or $\lambda U^-$. + +%% \begin{theorem} +%% EpCCω can encode System-F$_\omega$. +%% \end{theorem} +%% \begin{proof} +%% %% If we try to encode +%% %% +%% %% Λ(t:*).Λ(tf:*→*).λ(x:tf t).x +%% %% +%% %% (l₁) ≡> (t₁:Type l₁) -> (l₂) ≡> (t₂:Type l₂) -> +%% %% (l₃) ≡> (tf: (l₄) ≡> (_ : Type l₄) -> (l₅) ≡> (_ : Type l₅) +%% %% -> Type l₃) -> +%% %% tf {l₁} t₁ {l₂} t₂ +%% We take as input a stratified version of System-F$_\omega$, so +%% as to make an encoding based purely on the syntax rather than the typing +%% derivation. +%% \begin{displaymath} +%% \begin{array}{lccl} +%% \textsl{(kinds)} & \kappa &::=& * ~|~ \kappa_1\to\kappa_2 %% ~|~ (x:\tau) \to \kappa +%% \ +%% \textsl{(types)} & \tau &::=& +%% t ~|~ \tau_1\to\tau_2 ~|~ (t:\kappa)\to\tau +%% ~|~ \lambda t:\kappa.\tau ~|~ \tau_1~\tau_2 %% ~|~ \lambda x:\tau_1.\tau_2 ~|~ \tau~e +%% \ +%% \textsl{(terms)} & e &::=& +%% x ~|~ \lambda x:\tau.e ~|~ e_1~e_2 ~|~ \lambda t:\kappa.e ~|~ e~\tau +%% \end{array} +%% \end{displaymath} +%% \newcommand\Ftoa{\MetaFunction{}} +%% Then we define the encoding $\MetaFunction{}{\cdot}$ from System-F$_\omega$ to EpCCω: +%% %% FIXME: +%% %% What about Λt₁.Λt₂.id[t₁→t₂→t₁](λx:t₁→λy:t₂→x) ? +%% %% That should turn into +%% %% +%% %% (l₁:Level) ≡> (t₁:Type l₁) → +%% %% (l₂:Level) ≡> (t₂:Type l₂) → +%% %% id (l₁⊔l₂) (t₁→t₂→t₁) (λx:t₁→λy:t₂→x) +%% \begin{displaymath} +%% \begin{array}{r@{~=~}ll} +%% \MetaFunction{}{\bullet} & \bullet~;~\bullet \ +%% \MetaFunction{}{\Gamma,x:\tau} & +%% \Gamma',x:\MetaFunction{}{\tau} ~;~ \Delta& +%% \text{where }\Gamma';\Delta = \MetaFunction{}{\Gamma}\ +%% %% \MetaFunction{s}{\Gamma,t:\kappa} & +%% %% \MetaFunction{s}{\Gamma},t:\MetaFunction{s}{\kappa} \ +%% \MetaFunction{}{\Gamma,t:*} & +%% \Gamma',l:\kw{Level},t:\Type{l} ~;~ \Delta,t:l & +%% \text{where }\Gamma';\Delta = \MetaFunction{}{\Gamma} +%% \medskip \ +%% \MetaFunction{\Delta}{t} & t ~;~ \Delta(t) \ +%% \MetaFunction{\Delta}{\tau_1\to\tau_2} & +%% \ArwS[n]{\tau_1'}{\tau_2'} +%% ~;~ \Tlub{\ell_1}{\ell_2}& +%% \text{where } \tau_1';\ell_1 = \MetaFunction{\Delta}{\tau_1} +%% \text{ and } \tau_2';\ell_2 = \MetaFunction{\Delta}{\tau_2}\ +%% \MetaFunction{\Delta}{(t:*)\to\tau} & +%% \Arw[e]{l}{\kw{Level}}{ +%% \Arw[n]{t}{\Type{l}}{ +%% \tau'}} ~;~ \ell' & +%% \text{where } \tau';\ell = \MetaFunction{\Delta,t:l}{\tau} +%% \text{ and } \ell' = \Tlub{1!!}{!!\Subst{\ell}{0}{l}} +%% \medskip \ +%% \MetaFunction{\Delta}{x} & x \ +%% \MetaFunction{\Delta}{\lambda x:\tau . e} & +%% \Lam[n]{t}{\tau'}{\MetaFunction{\Delta}{e}} & +%% \text{where }\tau';\ell = \MetaFunction{\Delta}{\tau} \ +%% \MetaFunction{\Delta}{e_1~e_2} & +%% \App[n]{\MetaFunction{\Delta}{e_1}}{\MetaFunction{\Delta}{e_2}} \ +%% \MetaFunction{\Delta}{\lambda t:*.e} & +%% \Lam[e]{l}{\kw{Level}}{ +%% \Lam[n]{t}{\Type{l}}{ +%% \MetaFunction{\Delta,t:l}{e}}} \ +%% \MetaFunction{\Delta}{e~\tau} & +%% \App[n]{(\App[e]{\MetaFunction{\Delta}{e}}{\ell})}{ +%% \tau'} & +%% \text{where } \tau';\ell = \MetaFunction{\Delta}{\tau} +%% \medskip \ +%% %% \MetaFunction{s}{(t:\kappa_1)\to\kappa_2} & +%% %% \Arw[n]{t}{\MetaFunction{s}{\kappa_1}}{\MetaFunction{s}{\kappa_2}} \ +%% %% \MetaFunction{s}{\lambda t:\kappa . \tau} & +%% %% \Lam[n]{t}{\MetaFunction{s}{\kappa}}{\MetaFunction{s}{\tau}} \ +%% %% \MetaFunction{s}{\tau_1~\tau_2} & +%% %% \App[n]{\MetaFunction{s}{\tau_1}}{\MetaFunction{s}{\tau_2}} \ +%% %% \cdots&\cdots \ +%% \end{array} +%% \end{displaymath} +%% And then we can show by structural induction on the type derivation that +%% for any $\Jtype{e}{\tau}$ in System-F, we have $\Jtype[\Gamma']{e'}{\tau'}$ and +%% $\Jtype[\Gamma']{\tau'}{\Type{\ell}}$ in EpCCω where $\Gamma';\Delta = \MetaFunction{}{\Gamma}$, $e' +%% = \MetaFunction{\Delta}{e}$, and $\tau';\ell = \MetaFunction{\Delta}{\tau}$. +%% \end{proof} + %% \section{Related work}

%% \nocite{Gimenez94}

===================================== refs.bib ===================================== @@ -481,6 +481,42 @@ year = {1995}, }

+@inproceedings{Chlipala08, + address = {Victoria, BC}, + author = {Adam Chlipala}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'08}, + month = sep, + title = {Parametric Higher-Order Abstract Syntax for + Mechanized Semantics}, + year = {2008}, + abstract = {We present parametric higher-order abstract syntax + (PHOAS), a new approach to formalizing the syntax of + programming languages in computer proof assistants + based on type theory. Like higher-order abstract + syntax (HOAS), PHOAS uses the meta language's binding + constructs to represent the object language's binding + constructs. Unlike HOAS, PHOAS types are definable in + general-purpose type theories that support + traditional functional programming, like Coq's + Calculus of Inductive Constructions. We walk through + how Coq can be used to develop certified, executable + program transformations over several statically-typed + functional programming languages formalized with + PHOAS; that is, each transformation has a + machine-checked proof of type preservation and + semantic preservation. Our examples include CPS + translation and closure conversion for simply-typed + lambda calculus, CPS translation for System F, and + translation from a language with ML-style pattern + matching to a simpler language with no variable-arity + binding constructs. By avoiding the syntactic hassle + associated with first-order representation + techniques, we achieve a very high degree of proof + automation.}, + url = {http://adam.chlipala.net/papers/PhoasICFP08/%7D, +} + @proceedings{FOSSACS08, address = {Budapest, Hungary}, booktitle = {Conference on Foundations of Software Science and @@ -505,6 +541,15 @@ year = {2009}, }

+@proceedings{ICFP08, + address = {Victoria, BC}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'08}, + month = sep, + title = {International Conference on Functional Programming}, + year = {2008}, +} + @proceedings{LICS86, booktitle = {Annual Symposium on Logic in Computer Science}, key = {LICS'86},

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