Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
% !TeX root = slides.tex
\section{Conclusion}
\begin{frame}{Overall Summary}
\structure{Logical Relations:}
\begin{itemize}
\item many type theories admit this proof technique:\begin{enumerate}
\item map every type $\tpName$ to an $n$-ary relation $C_{\tpName}(-)$
\item prove that every constructor $f\colon\tpName_1\to\ldots\to\tpName_n\to\tpName$ preserves the relation $C_{\tpName}(-)$
\end{enumerate}
\item ``the basic lemma'': if $t\colon\tpName$, then $C_{\tpName}(t)$
\end{itemize}
\medskip
\structure{Concretely in \mmt/LF:} for morphisms $\mu_1,\ldots,\mu_n\colon S \to T$
\[
\logrel{r}{\mu_1 \times \cdots \times \mu_n}{S}{T}
\]
\vspace{-1.5em}
\begin{itemize}
\item special case for morphisms being identities: \begin{itemize}
\item $\nakedLogRel{\TND}{\id{PL}}{\PL}{\PL}$: unary congruence proving $p\colon\prop \Longrightarrow\;\vtnd{p}$
\item $\nakedLogRel{\LRA}{\id{PL}\times\id{\PL}}{\PL}{\PL}$: (binary) congruence whose well-typedness shows $\Leftrightarrow$ being a congruence
\end{itemize}
%
\item special case
\vspace{-0.5em} \[
\logrel{\TypePres}{\TypeEras}{\ChurchProd}{\CurryProd}
\]
\vspace*{-1em}
\begin{itemize}
\item complements lossy translation $\TypeEras$
\item $\vdash_{\ChurchProd} t \colon \ttm{A} \;\;\Longrightarrow\;\;\vdash_{\CurryProd} \wit\colon\ofType{\TypeEras(t)}{\TypeEras(A)}$
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}{Future Work}
\ldots
\end{frame}