\documentclass[12pt]{beamer}
\usepackage[latin9]{inputenc}
\usepackage{logictheme}
\usefonttheme[onlymath]{serif}
%%%%% Bug in beamer
\makeatletter
\SetSymbolFont{operators}{normal}{OT1}{cmr}{m}{n}
  \ifx\mv@bold\@undefined
  \else
    \SetSymbolFont{operators}{bold}{OT1}{cmr}{bx}{n}
  \fi
\makeatother

\usecolortheme[rgb={0.5,0.3,0}]{structure}
%\setbeamercolor{normal text}{fg=white,bg=black}
%\setbeamercolor{subsection in toc}{fg=white}
%\setbeamercolor{palette secondary}{fg=white}

\setbeamertemplate{theorems}[ams style]

\newtheorem{conjecture}{Conjecture}
\newtheorem{proposition}[theorem]{Proposition}
%\setbeamercolor{titlelike} 
%	       {use={palette primary},fg=black,bg=palette
%		 primary.bg} 

%\input{entete}
%\input{/Users/gburel/asbi/aacs/macros_modified}
%\input{sequents}
\usepackage{bussproofs}
\input{pts_def}
\input{natded}
   
\renewcommand{\S}{\mathcal S}
\newcommand{\A}{\mathcal A}
\newcommand{\R}{\mathcal R}

\newcommand{\one}{\textsf{\upshape 1}}
\newcommand{\esubst}[2]{#1\left[#2\right]}
\newcommand{\sigmanf}[1]{\sigma\left(#1\right)}

\newcommand{\lift}{\textsf{\upshape lift}}
\newcommand{\cons}{\textsf{\upshape cons}}
\newcommand{\shift}{\textsf{\upshape shift}}

\newcommand{\inc}[2]{\epsilon\left(#1,#2\right)}
\newcommand{\type}{\textsf{type}}
\newcommand{\kind}{\textsf{kind}}
\newcommand{\pitype}[2]{\dot\pi_{\type}\left(#1,#2\right)}
\newcommand{\pikind}[2]{\dot\pi_{\kind}\left(#1,#2\right)}
\newcommand{\pis}[2]{\dot\pi_{s}\left(#1,#2\right)}
\newcommand{\pisss}[3]{\dot\pi_{\langle #1,#2,#3\rangle}}
\newcommand{\pia}[3][\pisss{s_1}{s_2}{s_3}]{#1\left(#2,#3\right)}
\newcommand{\s}{\textsf{\textup{s}}}
\newcommand{\sone}{\s_{\textsf{1}}}
\newcommand{\stwo}{\s_{\textsf{2}}}
\newcommand{\sthree}{\s_{\textsf{3}}}

\newcommand{\length}{\overline}
\newcommand{\transn}[2][]{|#2|_{#1}}
\def\transa[#1][#2]#3{\transn[#2]{#3}^{#1}}
\makeatletter
\def\transab[#1]{\@ifnextchar[{\transa[#1]}{\transn[#1]}}
\def\trans{\@ifnextchar[{\transab}{\transn}}
\makeatother

\newcommand{\LB}{\textsf{\upshape LB}}
\newcommand{\LJp}{\textsf{\upshape LJ$^+$}}
\newcommand{\LBp}{\LB$^+$}
\newcommand{\LKp}{\textsf{\upshape LK$^+$}}
\newcommand{\NJp}{\textsf{\upshape NJ$^+$}}
\let\fCenter\vdash

\providecommand{\subst}[3]{\{#2/#3\}#1}
\providecommand{\df}{\stackrel{\text{\tiny def}}=}
\providecommand{\imp}{\Rightarrow}
\providecommand{\rewrite}{\mathop{\longrightarrow}\limits}
\providecommand{\leftrewrite}{\mathop{\longleftarrow}\limits}
\providecommand{\sRewrite}{\mathop{\longleftrightarrow}\limits}
\providecommand{\vect}[2][n]{#2_1,\ldots,#2_{#1}}
\newcommand{\Crabbe}{\mathcal C}

\providecommand{\Def}{\emph}

\newenvironment{super}{\let\oldFCenter\fCenter\def\fCenter{\vdash\lower-8pt\hbox{\kern-8pt{\scriptsize$+$}}}}{\def\fCenter{\oldFCenter}}

\newenvironment{lp}{\let\oldFCenter\fCenter\def\fCenter{\vdash\lower4pt\hbox{\kern-8pt{\scriptsize$\lambda\Pi$}}\,}}{\def\fCenter{\oldFCenter}}

\newenvironment{pts}{\let\oldFCenter\fCenter\def\fCenter{\vdash\nolinebreak\lower4pt\hbox{\kern-6pt{\scriptsize
        \textnormal{PTS}}}\,}}{\def\fCenter{\oldFCenter}}

\newcommand{\AxiomD}{\noLine\UnaryInf}

\title{Superdeduction as a Logical Framework}
\subtitle[GEOCAL/LAC]{Réunion des groupes de travail\\
GEOCAL et
LAC du
GDR IM}
\author{Guillaume Burel}
\date[2008-03-07]{Friday March 7th, 2008}
\institute[Nancy-U/LORIA]{Nancy-Université -- LORIA {\small(INRIA)}}
\setbeamertemplate{caption}[numbered]
\logo{\includegraphics[height=.06\textheight]{loria.jpg}\hspace{.04\textheight}\includegraphics[height=.06\textheight]{logo_uhp_blanc.jpg}}

%\includeonlyframes{current}
  
\begin{document}

\begin{frame}
\titlepage
\end{frame}

\section{Introduction}
\subsection{Logical Frameworks}
\begin{frame}
\frametitle{Definition}
  \cite{pfenning96practice}: 

``A logical framework is a
meta-language for the specification of deductive systems.''
\medskip\pause

The canonical logical framework is the one from Edinburgh
\cite{harper93framework}.

Based on the $\lambda$-calculus with dependent types: $\lambda P$ or $\lambda\Pi$
\end{frame}

\begin{frame}
  \frametitle{Example}
First-order natural deduction in ELF:

$$
\begin{array}{l}
\iota:*\\
o: *\\
\dot\neg:o\imp o\\
\dot\imp:o\imp o\imp o\\
\dot\forall:(\iota\imp o)\imp o
\end{array}
$$
\pause
$$|\forall x.~\phi|_\ell = (\dot\forall~\lambda x:\iota~|\phi|_{x::\ell})$$
\pause
$$
\begin{array}{l}
true:o\imp *\\
  \forall_I:\Pi f:\iota\imp o~(\Pi x:\iota~(true~(f~x)))\imp
  (true~(\dot\forall~\lambda x:\iota~(f~x)))
\end{array}
$$
\end{frame}
\subsection{Superdeduction}
\begin{frame}
  \frametitle{Superdeduction}
Opposite approach to LF

From (the presentation of) a theory is computed a deductive system  

Example: 

$\forall a~b.~a\subseteq b\Leftrightarrow(\forall x.~x\in
a\imp x\in b)$
\smallskip

  \Axiom$\Gamma,x\in a\fCenter x\in b$
  \URule[\scriptsize
    \begin{tabular}{@{}l@{}}
      $x$ not\\ free in $\Gamma$
    \end{tabular}
  ]{\irule{\subseteq^{\text{df}}}}$\Gamma\fCenter a\subseteq b$
\DisplayProof\hfill\Axiom$\Gamma\fCenter a\subseteq b$ \Axiom$\Gamma\fCenter t\in a$
\BiRule{\erule{\subseteq^{\text{df}}}}$\Gamma\fCenter t\in b$\DisplayProof
\end{frame}

\begin{frame}
  \frametitle{Superdeduction as a Logical Framework}

But superdeduction can be seen as a LF:

From a deductive system, find a first-order theory such that the
superdeductive system corresponds to it

Already done for HOL~\cite{hollambdasigma}

Here: for functional Pure Type Systems

\end{frame}

\begin{frame}
  \frametitle{PTS in superdeduction}
  \begin{itemize}
  \item Show that superdeduction is expressive as a logical framework
  \item Apply well-studied first-order methods to PTS\\(see also \cite{stehr04PTS})
  \item Cooperation between proof assistants
  \item New approach to normalization in PTS ?
  \end{itemize}
\end{frame}

\begin{frame}[label=context]
    \begin{center}
\only<1>{\input{context_1.pdf_t}}%
\only<2>{\input{context_1_5.pdf_t}}%
\only<3>{\input{context_2_pts.pdf_t}}%
\only<4>{\input{context_3_pts.pdf_t}}%
\only<5>{\input{context_pts.pdf_t}}%
~~~~~~~~~~~~~~
  \end{center}
\end{frame}



\AtBeginSection[]{
\begin{frame}
\frametitle{Outline} 
\tableofcontents[currentsection] 
\end{frame} 
} 

\section{Natural Superdeduction}

\begin{frame}
  \frametitle{Input theory}
  A first-order theory, presented as a rewrite system whose rules
  \begin{itemize}
  \item rewrite terms to terms
  \item or rewrite atomic propositions to first-order formul\ae
  \end{itemize}
\medskip

Examples:
$$x + s(y) \rightarrow s(x + y)$$
$$Singleton(p) \rightarrow \forall x,~\forall y,~x\in p\imp y\in
p\imp x = y$$
\end{frame}

\begin{frame}
  \frametitle{Computing introduction rules}
Proposition rewrite rule $A\rightarrow P$:

Apply all possible introduction rules to $P$

Create a new inference rule with $A$ as conclusion and the open leaves
as premises

Keep the side-conditions (freshness)
\end{frame}

\begin{frame}
  \frametitle{Example}
$$Singleton(p) \rightarrow \forall x,~\forall y,~x\in p\imp y\in
p\imp x = y$$
  \begin{prooftree}
    \Axiom$\Gamma,x\in p,y\in p\fCenter x = y$
    \ImpI$\Gamma,x\in p\fCenter y\in p\imp x = y$
    \ImpI$\Gamma\fCenter x\in p\imp y\in p\imp x = y$
    \AllI[\tiny$y$ not free in $\Gamma$]$\Gamma\fCenter\forall y,~x\in
    p\imp y\in p\imp x = y$
    \AllI[\tiny$x$ not free in $\Gamma$]$\Gamma\fCenter\forall x,~\forall y,~x\in
    p\imp y\in p\imp x = y$
  \end{prooftree}
\pause

  \begin{super}
    \begin{prooftree}
      \Axiom$\Gamma,x\in p,y\in p\fCenter x = y$
      \URule[\tiny
        \begin{tabular}{l}
          $x$ not free in $\Gamma$\\
          $y$ not free in $\Gamma$
        \end{tabular}
      ]{\irule{Singl^{\text{def}}}}$\Gamma\fCenter Singleton(p)$
    \end{prooftree}
  \end{super}
\end{frame}

\begin{frame}
  \frametitle{Computing elimination rules}
Proposition rewrite rule $A\rightarrow P$:

Apply all possible elimination rules to $P$, keeping new assumptions

Create a new inference rule with $A$ as first premise, the other open leaves
as premises, and the same conclusion
\end{frame}

\begin{frame}
  \frametitle{Example}
$$Singleton(p) \rightarrow \forall x,~\forall y,~x\in p\imp y\in
p\imp x = y$$
  \begin{prooftree}
 \Axiom$\Gamma\fCenter\forall x,~\forall y,~x\in p\imp y\in
p\imp x = y$
\AllE$\Gamma\fCenter\forall y,~t\in p\imp y\in
p\imp t = y$
\AllE$\Gamma\fCenter t\in p\imp u\in
p\imp t = u$
\Axiom$\Gamma\fCenter t\in p$
\insertBetweenHyps{}
\ImpE$\Gamma\fCenter u\in
p\imp t = u$
\Axiom$\Gamma\fCenter u\in p$
\insertBetweenHyps{}
\ImpE$\Gamma\fCenter t = u$
  \end{prooftree}
\pause

  \begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter Singleton(p)$
      \Axiom$\Gamma\fCenter t\in p$
      \Axiom$\Gamma\fCenter u\in p$
      \TriRule{\erule{Singl^{\text{def}}}}$\Gamma\fCenter t=u$
    \end{prooftree}
  \end{super}
\end{frame}

\begin{frame}
  \frametitle{Equivalence}
All inference rules (new and logical) are applied modulo the term
rewrite system

\begin{proposition}[{\cite{wack06supernatural}}]
  For a theory $\mathcal T$ corresponding to the considered rewrite
  system,

  \begin{center}
    $\mathcal T \fCenter P$ iff \begin{super}$~\fCenter P$\end{super}
  \end{center}
\end{proposition}

For $P(x)\rightarrow Q(x)$, theory: $\forall x,~P(x)\Leftrightarrow Q(x)$

\end{frame}

\section{Pure Type Systems}
\begin{frame}
  \frametitle{Pure type systems}
  \begin{itemize}
  \item A set of sorts $\S$
\item A binary relation $\A\subseteq\S\times\S$ (axioms)
\item A trinary relation $\R\subseteq\S\times\S\times\S$ (rules)

  \end{itemize}
Functional PTS: $\A$ and $\R$ defines (partial) functions from $\S$
and $\S\times\S$ to $\S$

\end{frame}

\begin{pts}
  \begin{frame}
    \frametitle{Typing system}
\begin{prooftree}    \Empty{$[]$ well-formed}
      \end{prooftree}
\begin{prooftree}

\Axiom$\Gamma\fCenter A:s$
        \Declaration[$s\in\S$ and $x$ not in $\Gamma$]{$\Gamma[x:A]$ well-formed}
      \end{prooftree}
\begin{prooftree}

\AxiomC{$\Gamma$ well-formed}
        \Sort[$\langle s_1,s_2\rangle\in\A$]$\Gamma\fCenter s_1:s_2$
      \end{prooftree}
\begin{prooftree}

        \AxiomC{$\Gamma$ well-formed}
        \AxiomC{$x:A\in\Gamma$}
        \Variable$\Gamma\fCenter x:A$
      \end{prooftree}

  \end{frame}


\begin{frame}
  \frametitle{Typing system (cont.)}
\begin{prooftree}            \Axiom$\Gamma\fCenter A:s_1$
        \Axiom$\Gamma[x:A]\fCenter B:s_2$
        \Product[$\langle s_1,s_2,s_3\rangle\in\R$]$\Gamma\fCenter\Pi x:A~B:s_3$
      \end{prooftree}
\begin{prooftree}

      \Axiom$\Gamma\fCenter T:\Pi x:A~B$
        \Axiom$\Gamma\fCenter U:A$
        \Application$\Gamma\fCenter(T~U):\subst BUx$
      \end{prooftree}
\begin{prooftree}
\Axiom$\Gamma\fCenter \Pi x:A~B:s$
        \Axiom$\Gamma[x:A]\fCenter T:B$
        \Abstraction$\Gamma\fCenter\lambda x:A~T:\Pi x:A~B$
      \end{prooftree}
\begin{prooftree}

      \Axiom$\Gamma\fCenter T:A$
        \Axiom$\Gamma\fCenter B:s$
        \Conversion[$s\in\S$ and $A{\sRewrite^*}_\beta B$]$\Gamma\fCenter T:B$
    \end{prooftree}

\end{frame}
\end{pts}


\section{PTS in Supernatural Deduction}
\subsection{Encoding}
\begin{frame}
  \frametitle{First-order syntax}
Constant $\s$ for each sort $s\in\S$

Function symbol $\pisss{s_1}{s_2}{s_3}$ for each rule $\langle
s_1,s_2,s_3\rangle\in\R$

$\lambda$-calculus with explicit substitutions $\lambda_W$ following a
scheme~\cite{kesner99tcs} ensuring its confluence
\end{frame}


\begin{frame}
  \frametitle{Translations of terms}
\begin{itemize}
\item $\trans[\ell_1::x::\ell_2]{x}\df \underline{\length{\ell_1}+1}$
  if $x\not\in\ell_1$

\item  $\trans[\ell]{x}\df \esubst x{shift}^{\length{\ell}}$
  if $x\not\in\ell$

\item  $\trans[\ell]{s}\df \s$

\item  $\trans[\ell]{\lambda x:A~t}\df \lambda\trans[x::\ell]t$
  \medskip

\item  \large
  $\trans[\Gamma][\ell]{\Pi x:A~B}\df
  \pia{\trans[\Gamma][\ell]A}{\trans[\Gamma{[x:A]}][x::\ell]B}$
  where
  \begin{itemize}
  \item $s_1$ corresponds the type of $A$ in $\Gamma$\item $s_2$ the type
    of $B$ in $\Gamma[x:A]$ \item$\langle
    s_1,s_2,s_3\rangle\in\R$
  \end{itemize}
\end{itemize}
  
\end{frame}

\begin{frame}
  \frametitle{First-order theory}
Rules on terms:  $\lambda_W$ +
\begin{eqnarray*}
  \esubst{\s}{t} &\rightarrow& \s\\
\esubst{\pia ab}s &\rightarrow& \pia{\esubst as}{\esubst
  b{\lift (s)}}
\end{eqnarray*}

Rules on propositions:
\begin{eqnarray}
\label{prr:tk}\inc{\sone}{\stwo} &\rightarrow& \top\hspace{1.7cm}(\langle s_1,s_2\rangle\in\A)\\
\label{prr:pi}\inc{\pia ab}{\sthree} &\rightarrow& \inc a{\sone}\wedge\\
\nonumber&& \forall z.~\inc
za\imp\inc{\esubst b{\cons (z)}}{\stwo}\\
\label{prr:lambda}\inc t{\pia ab} &\rightarrow& \inc{\pia ab}{\sthree}\wedge\\
\nonumber&&\forall z.~\inc za\imp\inc
     {t~z}{\esubst b{\cons (z)}}
\end{eqnarray}
\end{frame}


\subsection{Resulting System}
\begin{frame}
\begin{equation*}
\tag{\ref{prr:tk}}\inc\sone\stwo ~\rightarrow~ \top
\end{equation*}

\begin{super}
  \begin{prooftree}
    \AxiomC{}\LeftLabel{\irule{(\ref{prr:tk})}}
    \UnaryInf$\Gamma\fCenter \inc\sone\stwo$
  \end{prooftree}
\end{super}

\begin{pts}
  \begin{prooftree}
    \AxiomC{$\Gamma$ well-formed}
    \Sort$\Gamma\fCenter s_1:s_2$
  \end{prooftree}
\end{pts}
\end{frame}

\begin{frame}

\begin{eqnarray}
\nonumber\inc{\pia ab}{\sthree} &\rightarrow& \inc a{\sone}\wedge\hspace{3.5cm}(\ref{prr:pi})\\
\nonumber&& \forall z.~\inc
za\imp\inc{\esubst b{\cons (z)}}{\stwo}
\end{eqnarray}


\begin{super}
  \begin{prooftree}
 \Axiom$\Gamma\fCenter\inc a{\sone}$
      \Axiom$\Gamma,\inc za\fCenter\inc{\esubst b{\cons (z)} }{\stwo}$
      \LeftLabel{\irule{(\ref{prr:pi})}}
      \RightLabel{\small $z\text{ not free in
        }\Gamma$}
      \BinaryInf$\Gamma\fCenter\inc{\pia ab}{\sthree}$
  \end{prooftree}
\end{super}

\begin{pts}
  \begin{prooftree}            \Axiom$\Gamma\fCenter A:s_1$
    \Axiom$\Gamma[x:A]\fCenter B:s_2$
    \Product[$\langle s_1,s_2,s_3\rangle\in\R$]$\Gamma\fCenter\Pi x:A~B:s_3$
  \end{prooftree}
\end{pts}
\end{frame}


\begin{frame}
\begin{eqnarray}
\nonumber\inc{\pia ab}{\sthree} &\rightarrow& \inc a{\sone}\wedge\hspace{3.5cm}(\ref{prr:pi})\\
\nonumber&& \forall z.~\inc
za\imp\inc{\esubst b{\cons (z)}}{\stwo}
\end{eqnarray}

\begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\inc{\pia ab}{\sthree}$
      \LeftLabel{\erule[1]{(\ref{prr:pi})}}
      \UnaryInf$\Gamma\fCenter\inc a{\sone}$
    \end{prooftree}
\end{super}

No corresponding inference rule in the PTS

Conservative because if $\pia ab$ is the translation of some PTS term
$\Pi x:A~B$, then $A$ has type $s_1$
\end{frame}

\begin{frame}
\begin{eqnarray}
\nonumber\inc{\pia ab}{\sthree} &\rightarrow& \inc a{\sone}\wedge\hspace{3.5cm}(\ref{prr:pi})\\
\nonumber&& \forall z.~\inc
za\imp\inc{\esubst b{\cons (z)}}{\stwo}
\end{eqnarray}

\begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\inc{\pia ab}{\sthree}$
      \Axiom$\Gamma\fCenter\inc ua$
      \LeftLabel{\erule[2]{(\ref{prr:pi})}}
      \BinaryInf$\Gamma\fCenter\inc {\esubst b{\cons (u)} }{\stwo}$
    \end{prooftree}
\end{super}

No corresponding inference rule in the PTS

Conservative because $\pia ab$ is the translation of some PTS term
$\Pi x:A~B$, then $B$ has type $s_2$ in $\Gamma[x:A]$ and by
substitution \begin{pts}
  $\Gamma\fCenter\subst BUx:s_2$
\end{pts}
\end{frame}

\begin{frame}
\begin{eqnarray*}
\inc t{\pia ab} &\rightarrow& \inc{\pia ab}{\sthree}\wedge\hspace{2cm}(\ref{prr:lambda})\\
\nonumber&&\forall z.~\inc za\imp\inc
     {t~z}{\esubst b{\cons (z)}}
\end{eqnarray*}

\begin{super}    \begin{prooftree}
      \Axiom$\Gamma\fCenter\inc{\pia ab}{\sthree}$
      \Axiom$\Gamma,\inc za\fCenter\inc{t~z}{\esubst b{\cons (z)} }$
      \LeftLabel{\irule{(\ref{prr:lambda})}}
      %\RightLabel{\small $z\text{ not free in }\Gamma$}
      \BinaryInf$\Gamma\fCenter\inc t{\pia ab}$
    \end{prooftree}
\end{super}


\begin{pts}
  \begin{prooftree}
    \Axiom$\Gamma\fCenter \Pi x:A~B:s_3$
    \Axiom$\Gamma[x:A]\fCenter T:B$
    \Abstraction$\Gamma\fCenter\lambda x:A~T:\Pi x:A~B$
  \end{prooftree}
\end{pts}
Need for subject reduction  for $\eta$

\end{frame}

\begin{frame}
\begin{eqnarray*}
\inc t{\pia ab} &\rightarrow& \inc{\pia ab}{\sthree}\wedge\hspace{2cm}(\ref{prr:lambda})\\
\nonumber&&\forall z.~\inc za\imp\inc
     {t~z}{\esubst b{\cons (z)}}
\end{eqnarray*}

\begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\inc t{\pia ab}$
      \LeftLabel{\erule[1]{(\ref{prr:lambda})}}
      \UnaryInf$\Gamma\fCenter\inc{\pia ab}{\sthree}$
    \end{prooftree}
\end{super}

No corresponding inference rule in the PTS

Conservative because if $\pia ab$ is the translation of some PTS term
$\Pi x:A~B$, then $A$ has type $s_1$ in $\Gamma$, $B$ has type $s_2$ in 
$\Gamma[x:A]$, hence $\Pi x:A~B$ has type $s_3$

\end{frame}

\begin{frame}
\begin{eqnarray*}
\inc t{\pia ab} &\rightarrow& \inc{\pia ab}{\sthree}\wedge\hspace{2cm}(\ref{prr:lambda})\\
\nonumber&&\forall z.~\inc za\imp\inc
     {t~z}{\esubst b{\cons (z)}}
\end{eqnarray*}

\begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\inc t{\pia ab}$
      \Axiom$\Gamma\fCenter\inc ua$
      \LeftLabel{\erule[2]{(\ref{prr:lambda})}}
      \BinaryInf$\Gamma\fCenter\inc {t~u}{\esubst b{\cons (u)} }$
    \end{prooftree}
\end{super}
\begin{pts}
  \begin{prooftree}

    \Axiom$\Gamma\fCenter T:\Pi x:A~B$
    \Axiom$\Gamma\fCenter U:A$
    \Application$\Gamma\fCenter(T~U):\subst BUx$
  \end{prooftree}
\end{pts}
\end{frame}

\subsection{Soundness and conservativeness}
\begin{frame}
\frametitle{Soundness}  
\begin{theorem}
  For all contexts $\Gamma$, for all PTS terms $A$ and $B$, if
  \begin{pts}$\Gamma\fCenter A:B$\end{pts}
  then 
  \begin{super}
    $|\Gamma| \fCenter \inc{|A|}{|B|}$\end{super}.
\end{theorem}
Remaining inference rules:
\begin{itemize}
\item \textrule{Variable}: through \textrule{Axiom}
\item \textrule{Conversion}: modulo the term rewrite system
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Conservativeness}
  \begin{theorem}
    For all \alert<2>{well-formed} contexts $\Gamma$, for all terms $a$, $b$,

 if 
 \begin{super}
   $|\Gamma| \fCenter \inc{a}{b}$
 \end{super}
 then there exists $A$ and $B$ such
 that 
 \begin{itemize}
 \item $a\rewrite^*|A|^\Gamma$
 \item $b\rewrite^*|B|^\Gamma$ 
 \item 
   \begin{pts}
     $\Gamma\fCenter A:B$
   \end{pts}
 \end{itemize}
  \end{theorem}
\end{frame}

\section{Normalization}
\subsection{Proof terms}
\begin{frame}
  \frametitle{Proof terms}
  Proof terms for superdeduction are particular $\rho$-terms

In this case, we need function symbols $R_1$, $R_2$ and $R_3$

\begin{super}
  \begin{prooftree}
    \AxiomC{}\LeftLabel{\irule{(\ref{prr:tk})}}
    \UnaryInf$\Gamma\fCenter \alert{R_1:}\inc\sone\stwo$
  \end{prooftree}
\end{super}
\end{frame}

\begin{frame}
  \frametitle{Proof terms for (\ref{prr:pi})}
  \begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\alert{M:}\inc a{\sone}$
      \Axiom$\Gamma,\alert{\alpha:}\inc za\fCenter\alert{N:}\inc{\esubst b{\cons (z)} }{\stwo}$
      \LeftLabel{\irule{(\ref{prr:pi})}}
      %      \RightLabel{\small $z\text{ not free in }\Gamma$}
      \BinaryInf$\Gamma\fCenter\alert{\lambda
        R_2(z,\alpha,y).~y\langle M,N\rangle:}
      \inc{\pia ab}{\sthree}$
    \end{prooftree}
  \end{super}
  
\begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\alert{M:}\inc{\pia ab}{\sthree}$
      \LeftLabel{\erule[1]{(\ref{prr:pi})}}
      \UnaryInf$\Gamma\fCenter\alert{M~R_2(z,\alpha,\lambda\langle x,y\rangle.~x):}\inc a{\sone}$
    \end{prooftree}
\end{super}
\begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\alert{M:}\inc{\pia ab}{\sthree}$
      \Axiom$\Gamma\fCenter\alert{N:}\inc ua$
      \LeftLabel{\erule[2]{(\ref{prr:pi})}}
      \BinaryInf$\Gamma\fCenter\alert{M~R_2(u,N,\lambda\langle x,y\rangle.~y):}\inc {\esubst b{\cons (u)} }{\stwo}$
    \end{prooftree}
\end{super}
\end{frame}
\begin{frame}
  \frametitle{Proof terms for (\ref{prr:lambda})}
  
\begin{super}    \begin{prooftree}
      \Axiom$\Gamma\fCenter\alert{M:}\inc{\pia ab}{\sthree}$
      \AxiomD$\Gamma,\alert{\alpha:}\inc za\fCenter\alert{N:}\inc{t~z}{\esubst b{\cons (z)} }$
      \LeftLabel{\irule{(\ref{prr:lambda})}}
      %\RightLabel{\small $z\text{ not free in }\Gamma$}
      \UnaryInf$\Gamma\fCenter\alert{\lambda
        R_3(z,\alpha,y).~y\langle M,N\rangle:}\inc t{\pia ab}$
    \end{prooftree}
\end{super}
\begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\alert{M:}\inc t{\pia ab}$
      \LeftLabel{\erule[1]{(\ref{prr:lambda})}}
      \UnaryInf$\Gamma\fCenter\alert{M~R_3(z,\alpha,\lambda\langle x,y\rangle.~x):}\inc{\pia ab}{\sthree}$
    \end{prooftree}
\end{super}

\begin{super}
    \begin{prooftree}
      \Axiom$\Gamma\fCenter\alert{M:}\inc t{\pia ab}$
      \Axiom$\Gamma\fCenter\alert{N:}\inc ua$
      \LeftLabel{\erule[2]{(\ref{prr:lambda})}}
      \BinaryInf$\Gamma\fCenter\alert{M~R_3(u,N,\lambda\langle x,y\rangle.~y):}\inc {t~u}{\esubst b{\cons (u)} }$
    \end{prooftree}
\end{super}
\end{frame}

\subsection{Equivalence of reductions ?}
\begin{frame}
  \frametitle{Reductions}
  $$(\lambda x.~T~U)\rewrite_\beta \subst TUx$$

$$(\lambda R_3(z,\alpha,y).~y\langle
  T_1,T_2\rangle)~R_3(u,N,\lambda\langle x,y\rangle.~y)
  \rewrite^2_\rho\subst{\subst {T_2}N\alpha}uz$$

What about other $\rho$-reductions ?
\end{frame}

\begin{frame}
  \frametitle{Conjecture}
  \begin{conjecture}
    A PTS is strongly normalizing iff the superdeductive system
    associated with it is.
  \end{conjecture}\pause
 \begin{proposition}
    A PTS is strongly normalizing if the superdeductive system
    associated with it is.
 \end{proposition}
Allow to use normalization methods for deduction modulo (premodel,
superconsistency)

\end{frame}


%% \section{Conclusion}
%% \begin{frame}<1>[label=summary]
%%   \frametitle{Summary}
%%   \begin{itemize}[<+->]
%%   \item Sound and conservative encoding of $\lambda\Pi$ in
%%     supernatural deduction
%%   \item Generic wrt $\lambda$-calculus with ES ($\lambda_\sigma$ can
%%     be used)
%%   \item Translations to/from super sequent calculus\pause,
%% \\ deduction modulo, pure natural deduction and sequent calculus, \ldots
%%   \end{itemize}

%% \end{frame}

%% \againframe<5>{context}
%% \againframe<2->{summary}
\section{Conclusion}
\begin{frame}
  \frametitle{Conclusion}
Quite natural encoding of functional PTS into supernatural deduction
\medskip 

Valid typing judgments = (reducts of) provable sequents 
\pause\medskip

Type checking = proof search
  

\end{frame}

\begin{frame}
  \frametitle{Perspectives}
  \begin{itemize}[<+->]
  \item Add new rules to check wellformedness of contexts
    (or pass the context into the term and type)
  \item Normalization:
    \begin{itemize}
    \item Prove conjecture
    \item Look at superconsistency
    \end{itemize}
  \item Add inductive types: as in CAC ?
  \item Add subtyping as in PVS
  \item Modify Lemurid\ae\ to deal with intuitionistic logic
  \item Encode more deductive systems using superdeduction:
    superdeduction as a logical framework
  \end{itemize}
\end{frame}



\bibliographystyle{apalike}
\bibliography{abbrev,burel,protheo,demons}

\end{document}

%%% Local Variables: 
%%%   mode: flyspell
%%% End: 
