Skip to content
Snippets Groups Projects
Commit 26f126cb authored by ghondet's avatar ghondet
Browse files

More

parent ee111778
No related branches found
Tags phdSlides@v1
No related merge requests found
......@@ -49,8 +49,8 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\usepackage{expl3}
\usepackage{xspace}
\newcommand\lpmr{\(\lambda\Pi\){/R}\xspace}
\newcommand\dk{\text{Dk}}
\newcommand\lpmr{\ensuremath{\lambda\Pi}{/R}\xspace}
\newcommand\lpTag{\ensuremath{\lambda\Pi}}
\newcommand\tr[1]{\left\llbracket #1 \right\rrbracket}
\newcommand\trA[1]{\left| #1 \right|}
\newcommand\trB[1]{\left\Vert #1 \right\Vert}
......@@ -186,6 +186,7 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\item Function reduction \hfill \(\tapp{(\tabst{x}x), 0} = 0\)
\item Arbitrary reductions \hfill \(\tapp*{\func{fst}, \tapp{\func{pair}, x, y}} = x\)
\end{itemize}
\onslide<+->
\begin{block}{Implementations}
\begin{description}[<+->]
\item[Dedukti] concrete syntax for \lpmr, parser + type checker
......@@ -195,7 +196,7 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{frame}
\begin{frame}{Embedding a system \(\mathcal{S}\) in \lpmr}
Sound (and complete) translation \([-]\) from \(\mathcal{S}\) to \lpmr.
Sound (and complete) embedding \([-]\) from \(\mathcal{S}\) to \lpmr.
\vfill
\setcounter{beamerpauses}{2}
......@@ -211,96 +212,56 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
% \begin{center} \verb+U = {z : complex | EXISTS (n: nat): z ** n = 1}+\end{center}
% \verb+e: U+ \hspace{2em} ``\(e \in \mathbb{C}\) and \(\exists n, e^n = 1\)''
% \end{block}
\begin{block}{}
\[ \{ n \in \mathbf{N} \mid 0 < n \} \]
\(\tcheck{}{1}{\{ n : \mathbf{N} \mid 0 < n \}}\) means `\(1 \in \mathbf{N}\) and \(0 < 1\)', but also\\
\(\tcheck{}{1}{\mathbf{N}}\)
\end{block}
\[ \tpsub{n}{\mathbf{N}}{0 < n} \]
\vfill
\onslide<+->
\begin{itemize}[<+->]
\item Expressive type-system
\item Concise and `intuitive' language
\end{itemize}
\vfill
\onslide<+->
\[ \tcheck{\Gamma}{1}{\tpsub{n}{\mathbf{N}}{0 < n}};\hspace{4em} \tcheck{\Gamma}{1}{\mathbf{N}} \]
\vfill
\pause
\onslide<+->
\begin{block}{PVS}
\begin{itemize}
\begin{itemize}[<+->]
\item Specification language + type checker + (semi) automated theorem prover
\item Used by Rockwell-Collins, Fujitsu, Stanford, NASA \&c.
\end{itemize}
\end{block}
\end{frame}
\begin{frame}{Introduction}
\begin{center}
\begin{tikzpicture}
\scriptsize
\node (PVS) {\textcolor{emph2}{PVS}};
\node[below right = 1.1cm of PVS] (Lp-PVS-subt)
{\(\mathrm{\textcolor{emph1}{Lp}[\textcolor{emph2}{PVS}]_{<}}\)};
\node[right = 1.1cm of Lp-PVS-subt] (Lp-PVS-meta)
{\(\mathrm{\textcolor{emph1}{Lp}[\textcolor{emph2}{PVS}]_{?}}\)};
\node[above = 0.4cm of Lp-PVS-meta] (provers) {Why3, \(\lambda\)Prolog, \emoji{writing-hand} };
\node[right = 1.1cm of Lp-PVS-meta] (Lp-PVS)
{\(\mathrm{\textcolor{emph1}{Lp}[\textcolor{emph2}{PVS}]}\)};
\node[right = 1.6cm of Lp-PVS] (Ok) { \emoji{check-mark} };
\draw[ultra thick,draw=ocre,fill=ocre,fill opacity=0.1]
(Lp-PVS-meta) ellipse (3.8cm and 1.2cm);
\node[below = 0.9cm of Lp-PVS-meta] {\textcolor{emph1}{Lambdapi}};
\path (provers.south) edge[bend right=20] (Lp-PVS.west);
\path (PVS.south) edge[bend right=30,->] (Lp-PVS-subt.west)
(Lp-PVS-subt) edge[->] (Lp-PVS-meta)
(Lp-PVS-meta) edge[->] (Lp-PVS)
(Lp-PVS) edge[->] (Ok)
;
\node[below = of Ok, xshift = -0.6cm] (Dk-PVS) {\textcolor{emph1}{Dk}[\textcolor{emph2}{PVS}]};
\node[right = of Dk-PVS] (sttfa) {\(\mathrm{STT}_\forall\)};
\node[below = of sttfa] (provers) {Coq, Lean, Matita, \dots};
\path (Lp-PVS.south) edge[bend right=40,->] (Dk-PVS.west)
(Dk-PVS) edge[->] (sttfa)
(sttfa.south) edge[->] (provers);
\path (Dk-PVS) edge[bend left=20,->] (Ok);
\node[right = 0.3cm of Dk-PVS] (Dk-centre) {};
\draw [ultra thick, draw = fuschia, fill = fuschia, fill opacity = 0.1]
(Dk-centre) ellipse (2cm and 0.8cm);
\node[below=of Dk-centre,yshift=0.3cm] {\textcolor{emph1}{Dedukti}};
\end{tikzpicture}
\end{center}
\end{frame}
\begin{frame}{Outline}
\tableofcontents
\end{frame}
\section{Explicit predicate subtyping}
\begin{frame}
\tableofcontents[currentsection]
\end{frame}
\begin{frame}{Simple type theory and predicate subtyping}
\[
t ::=
x \mid c \mid \tapp*{t, t} \mid \tabst{x}[t]t \mid \tprod[x]{t}t \mid \tprod{t}t
\onslide<3->{ \mid \tpsub{x}{t}{t} \mid \tapp{\tfst, t}}
\onslide<3->{ \mid \tpsub{x}{t}{t} \mid \tapp{\tpair, t, t} \mid \tapp{\tfst, t}}
\]
\onslide<2->{
\begin{empheq}{equation*}
\forall_{\iota} x, P \simeq \tprod[x]{\iota}P \hspace{4em} P \Rightarrow Q \simeq \tprod[x]{P}Q
\end{empheq}
\begin{center}
\begin{tabular}{ll}
STT & \(\lambda\)HOL \\
\toprule
\(\forall_{\iota} x, P\) & \(\tprod[x]{\iota}P\)\\
\(P \Rightarrow Q\) & \(\tprod[x]{P}Q\)
\end{tabular}
\end{center}
}
\onslide<4->{
\[
\tcheck
{\mathit{isPos}: \tprod[n]{\mathit{nat}} \tapp{\mathit{Pos}, (n + 1)}}
\tcheck[system=e]
{\mathit{isPos}: \tprod[n]{\mathbf{N}} \tapp{\mathit{Pos}, (n + 1)}}
{\tapp{\tpair, 1, {\tapp{\mathit{isPos}, 0}}}}
{\tpsub{n}{\mathit{nat}}{\tapp*{\mathit{Pos}, n}}}
{\tpsub{n}{\mathbf{N}}{\tapp*{\mathit{Pos}, n}}}
\]
}
\setcounter{beamerpauses}{5}
......@@ -326,7 +287,7 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{thebibliography}
\end{frame}
\begin{frame}{Encoding PVS-Cert in Dedukti}
\begin{frame}{Embedding PVS-Cert in \lpmr}
\begin{block}{}
\(\Set: \sType\)\\
\(\El: \Set \to \sType\)\\
......@@ -345,7 +306,7 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{frame}
\begin{frame}[fragile]
\frametitle{Principles of encodings in Dedukti}
\frametitle{Principles of embeddings in \lpmr}
\note{
\begin{itemize}
\item Technique used to encode CoC (say CoC because it is more widely known than PTSs) (in Cousineau article);
......@@ -355,9 +316,12 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{itemize}
}
\begin{tikzpicture}
[
term/.style={draw,ellipse,fill=white},
type/.style={draw=fuschia,ellipse,fill=white} ]
[ term/.style={draw,ellipse,fill=white}
, type/.style={draw=fuschia,ellipse,fill=white}
, pvsBoxes/.style = { draw = black, fill = ocre!5!white }
, pvsBigBox/.style = { pvsBoxes, rounded corners = 8pt }
, lpmrBoxes/.style = { fill = light-blue!5!white, draw = black }
, lpmrBigBox/.style = { lpmrBoxes, rounded corners = 8pt } ]
\node (rect-sysa-sw) at (0, 0) {};
\node (rect-sysa-nw) [above = \boxheight of rect-sysa-sw] {};
......@@ -367,13 +331,11 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\node (rect-sysb-nw) [above = \boxheight of rect-sysb-sw] {};
\node (rect-sysb-ne) [above right = \boxheight and \boxwidth of rect-sysb-sw] {};
\filldraw[fill=light-blue!5!white, draw=black, rounded corners=8pt]
(rect-sysa-sw) rectangle (rect-sysa-ne);
\node [draw,fill=light-blue!5!white] at (rect-sysa-nw.south) {Dedukti};
\filldraw [lpmrBigBox] (rect-sysa-sw) rectangle (rect-sysa-ne);
\node [lpmrBoxes] at (rect-sysa-nw.south) {\lpmr};
\filldraw[fill=ocre!5!white, draw=black, rounded corners=8pt]
(rect-sysb-sw) rectangle (rect-sysb-ne);
\node [draw,fill=ocre!5!white] at (rect-sysb-nw.south) {PVS};
\filldraw [pvsBigBox] (rect-sysb-sw) rectangle (rect-sysb-ne);
\node [pvsBoxes] at (rect-sysb-nw.south) {PVS};
\pause
......@@ -446,7 +408,7 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{column}
\begin{column}{0.5\textwidth}
\onslide<+->
If \(h_1 \ne h_2\), then \(z_1 \ne z_2\)
If \(h_1 \ne h_2\), then \(\alert{z_1 \ne z_2}\)
\end{column}
\end{columns}
......@@ -464,11 +426,11 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
If \(\tcheck[system=e]{\Gamma}{t}{T}\),\\
\vfill
\pause
then \(\tcheck[system=\dk]{[\Gamma]}{[t]}{\tapp*{\El, [T]}}\).
then \(\tcheck[system=\lpTag]{[\Gamma]}{[t]}{\tapp*{\El, [T]}}\).
\end{frame}
\begin{frame}{Preservation of typing}
\framesubtitle{Preservation of Computation}
\framesubtitle{Preservation of computation}
\newcommand\pieq{\ensuremath{\mathrel{\leftrightarrow^*_{\text{pi}}}}}
\newcommand\pieqS{\ensuremath{\mathrel{\leftrightarrow_{\text{pi}}}}}
......@@ -514,26 +476,53 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\begin{frame}{Completeness}
\begin{block}{Statement}
If \(\tcheck{\Gamma}{e_0}{\tapp*{\Prf, [P]}}\)\\
If \(\tcheck[system=\lpTag]{\Gamma}{e_0}{\tapp*{\Prf, [P]}}\)\\
then \(\tcheck[system=e]{\Delta}{e_1}{P}\)
\end{block}
\pause
\vfill
\begin{exampleblock}{Proof approaches}
\begin{itemize}[<+->]
\item termination + (Cousineau \& Dowek, 2007)
\item Termination (of embedding)+ (Cousineau \& Dowek, 2007)
\item (Assaf, 2015)
\item deep embeddings (Felicissimo, 2022)
\item Deep embeddings (Felicissimo, 2022)
\end{itemize}
\end{exampleblock}
\end{frame}
\begin{frame}{Example}
\(\func{stack}: \Set\)\\
\(\func{empty}: \tapp*{\El, \func{stack}}\)\\
\(\func{isNonEmpty} \coloneqq \tabst{s}s \ne \func{empty}\)\\
\(\func{nonEmpty} \coloneqq \tapp*{\epsub, \func{stack}, \func{isNonEmpty}}\)\\
\(\func{push}: \tapp*{\El, (\mathbf{N} \earr \func{stack} \earr \func{nonEmpty})}\)\\
\(\func{pop}: \tapp*{\El, (\func{nonEmpty} \earr \func{stack})}\)\\
\(\func{top}: \tapp*{\El, (\func{nonEmpty} \earr \mathbf{N})}\)\\
\begin{exampleblock}{}
\(\func{pushTopPop}: \Prf\)\\
\hspace{2ex}\(\eall\, \func{stack}\, (\lambda s, \tapp{\func{isNonEmpty}, s} \eimp\)\\
\hspace{2ex}\(\tapp*{\efst, \tapp{\func{push}, \tapp{\func{top}, \tapp{\epair, s, ?}}, \tapp{\func{pop}, \tapp{\epair, s, ?}}}} = s)\)
\end{exampleblock}
\end{frame}
\section{Implicit predicate subtyping}
\begin{frame}
\tableofcontents[currentsection]
\end{frame}
\begin{frame}{Implicitness}
\begin{exampleblock}{}
\(\tapp*{\efst, \tapp{\func{push}, \tapp{\func{top}, \tapp{\epair, s, {?_1}}}, \tapp{\func{pop}, \tapp{\epair, s, {?_2}}}}} = s\)
\end{exampleblock}
\vfill
\pause
\begin{block}{}
\(\tapp*{\func{push}, \tapp{\func{top}, s}, \tapp{\func{pop}, s}} = s\)
\end{block}
\end{frame}
\begin{frame}{Baked-in subtyping}
\[
\begin{prooftree}
......@@ -630,13 +619,13 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{columns}
\end{frame}
\begin{frame}{Going online (feat.\ rewriting, cont'd)}
\begin{frame}{Going on line (feat.\ rewriting, cont'd)}
\begin{center}
\(
\inferrule{
\tcheck[dir=infer,system=\dk]{\Gamma}{t}{T} \\ T \simeq U
\tcheck[dir=infer,system=\lpTag]{\Gamma}{t}{T} \\ T \simeq U
}{
\tcheck[dir = check, system = \dk]{\Gamma}{t}{U}
\tcheck[dir = check, system = \lpTag]{\Gamma}{t}{U}
}
\)\\
\vfill
......@@ -645,9 +634,9 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\vfill
\(
\inferrule{
\tcheck[dir=infer, system=\dk]{\Gamma}{t}{T} \\
\tapp{\kappa, T, U} \rw f \\ \tcheck[dir = check, system=\dk]{\Gamma}{\tapp{f, t}}{U}
}{ \tcheck[dir = check, system=\dk]{\Gamma}{t}{U} }
\tcheck[dir=infer, system=\lpTag]{\Gamma}{t}{T} \\
\tapp{\kappa, T, U} \rw f \\ \tcheck[dir = check, system=\lpTag]{\Gamma}{\tapp{f, t}}{U}
}{ \tcheck[dir = check, system=\lpTag]{\Gamma}{t}{U} }
\)
\pause
\note{No need for the premise \(\kappa \not\in f\) here because \(\kappa\) is not typeable anyway}
......@@ -673,8 +662,8 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\begin{frame}{Typing preservation}
If \(\tcheck[system=i]{\Gamma}{e}{T}\), then
\begin{itemize}
\item \(\tcheck[dir = check, r = \hat{T}, system = \dk]{[\Gamma]}{[T]}{\Set}\)
\item \(\tcheck[dir = check, r = \hat{t}, system = \dk]{[\Gamma]}{[t]}{\tapp*{\El, \hat{T}}}\).
\item \(\tcheck[dir = check, r = \hat{T}, system = \lpTag]{[\Gamma]}{[T]}{\Set}\)
\item \(\tcheck[dir = check, r = \hat{t}, system = \lpTag]{[\Gamma]}{[t]}{\tapp*{\El, \hat{T}}}\).
\end{itemize}
\vfill
......@@ -693,6 +682,10 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\begin{frame}{Completing the equational theory}
% Show why surjective pairing is needed, potentially extrapolate to
% confluence of coercion system
\(\tcheck[dir = infer, r = {\tapp{(\tabst{x}[A]\tapp{f, \tapp{\epair, x, {?_0}}}), \tapp{\efst, 1}}}]
{1: \tapp{\epsub, \mathbf{N}, (< 0)}, \mathit{prec}: \tprod{\tapp{\epsub, \mathbf{N}, (< 0)}} \mathbf{N}}
{\tapp{(\tabst{x}[\mathbf{N}]\tapp{f, x}), 1}}
{\mathbf{N}}\)
\end{frame}
\section{Results: translation of PVS into Dedukti}
......@@ -751,6 +744,52 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{block}
\end{frame}
\begin{frame}{Introduction}
\begin{center}
\begin{tikzpicture}
\scriptsize
\node (PVS) {\textcolor{emph2}{PVS}};
\node[below right = 1.1cm of PVS] (Lp-PVS-subt)
{\(\mathrm{\textcolor{emph1}{Lp}[\textcolor{emph2}{PVS}]_{<}}\)};
\node[right = 1.1cm of Lp-PVS-subt] (Lp-PVS-meta)
{\(\mathrm{\textcolor{emph1}{Lp}[\textcolor{emph2}{PVS}]_{?}}\)};
\node[above = 0.4cm of Lp-PVS-meta] (provers) {Why3, \(\lambda\)Prolog, \emoji{writing-hand} };
\node[right = 1.1cm of Lp-PVS-meta] (Lp-PVS)
{\(\mathrm{\textcolor{emph1}{Lp}[\textcolor{emph2}{PVS}]}\)};
\node[right = 1.6cm of Lp-PVS] (Ok) { \emoji{check-mark} };
\draw[ultra thick,draw=ocre,fill=ocre,fill opacity=0.1]
(Lp-PVS-meta) ellipse (3.8cm and 1.2cm);
\node[below = 0.9cm of Lp-PVS-meta] {\textcolor{emph1}{Lambdapi}};
\path (provers.south) edge[bend right=20] (Lp-PVS.west);
\path (PVS.south) edge[bend right=30,->] (Lp-PVS-subt.west)
(Lp-PVS-subt) edge[->] (Lp-PVS-meta)
(Lp-PVS-meta) edge[->] (Lp-PVS)
(Lp-PVS) edge[->] (Ok)
;
\node[below = of Ok, xshift = -0.6cm] (Dk-PVS) {\textcolor{emph1}{Dk}[\textcolor{emph2}{PVS}]};
\node[right = of Dk-PVS] (sttfa) {\(\mathrm{STT}_\forall\)};
\node[below = of sttfa] (provers) {Coq, Lean, Matita, \dots};
\path (Lp-PVS.south) edge[bend right=40,->] (Dk-PVS.west)
(Dk-PVS) edge[->] (sttfa)
(sttfa.south) edge[->] (provers);
\path (Dk-PVS) edge[bend left=20,->] (Ok);
\node[right = 0.3cm of Dk-PVS] (Dk-centre) {};
\draw [ultra thick, draw = fuschia, fill = fuschia, fill opacity = 0.1]
(Dk-centre) ellipse (2cm and 0.8cm);
\node[below=of Dk-centre,yshift=0.3cm] {\textcolor{emph1}{Dedukti}};
\end{tikzpicture}
\end{center}
\end{frame}
\begin{frame}{Translation of Prelude}
\begin{table}
\caption{Amount of translated entities.}
......@@ -790,7 +829,7 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{frame}
\begin{frame}{On proof representations}
\begin{block}{Certificates -- Dedukti}
\begin{block}{Certificates -- \lpmr}
\setcounter{beamerpauses}{2}
\begin{description}[<+->]
\item[Data] terms
......@@ -912,15 +951,13 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
\end{frame}
\begin{frame}{Perspectives}
\begin{block}{Proof export}
\begin{itemize}
\item[\emoji{check-mark}] \(\text{PVS-Cert} \to \text{Dedukti}\) \hfill personoj
\item[\emoji{check-mark}] \(\frac{Q}{P} \mapsto \frac{\dots}{Q \Rightarrow P}\) \hfill personoj
\item[\emoji{check-mark}] \(\phi: \text{PVS-Cert} \to \text{STT}\) \hfill F.~Gilbert
\item[\emoji{check-mark}] ATP in Dedukti (FOL only) \hfill Y.~El~Haddad
\item[\emoji{thinking}] \(\psi: \text{STT} \to \text{PVS-Cert}\)
\end{itemize}
\end{block}
\begin{itemize}[<+->]
\item[\emoji{check-mark}] \(\text{PVS-Cert} \to \text{Dedukti}\) \hfill personoj
\item[\emoji{check-mark}] \(\frac{Q}{P} \mapsto \frac{\dots}{Q \Rightarrow P}\) \hfill personoj
\item[\emoji{check-mark}] \(\phi: \text{PVS-Cert} \to \text{STT}\) \hfill F.~Gilbert
\item[\emoji{check-mark}] ATP in Dedukti (FOL only) \hfill Y.~El~Haddad
\item[\emoji{thinking}] \(\psi: \text{STT} \to \text{PVS-Cert}\)
\end{itemize}
\end{frame}
\section*{Conclusion}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment