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
40
41
42
43
% !TeX root = slides.tex
\appendix
\section{Pointers and References}
\newcommand\afterItemSpace{\vspace{0.75em}}
\begin{frame}[allowframebreaks]{Further Pointers}
\begin{itemize}
\item \structure{Logical Relations:}\begin{itemize}
\item Concise and to-the-point proof of SN of STLC: \cite{ziliani_stlc_sn}
\afterItemSpace%
Note the relation for function types there is missing the condition of strong normalization, which I corrected for in my slides; if in doubt, compare with \cite{skorstengaard_log_rel}.
\item Another proof of SN of STLC: \cite{ahmed_log_rel} (videos), third-party transcript at \cite[ch.~2]{skorstengaard_log_rel}
\afterItemSpace%
Here, the lambda calculus is equipped with if-then-else constructs, too, making the proof a bit more complicated (on a first read).
After SN of STLC, Ahmed considers several extensions of STLC, among others, with recursive types and reference types,
and uses logical relations to prove meta theorems about them.
\item Unrelated, but interesting: connection of logical relations with automata simulations: \cite{stackexchange_log_rel_and_simulations}
\end{itemize}
\item \structure{Logical Frameworks:}\begin{itemize}
\item \mmt System: \cite{rabe:howto:14,RabMue:WADT18}
\item Edinburgh LF: \cite{HarperEtAl:affdl93}
\end{itemize}
\item \structure{Logical Relations for a Logical Framework:}\begin{itemize}
\item The article on which this talk is based: \cite{RS:logrels:12}
\item Proof of SN in Twelf: \cite{SchSar:structurallogrel}
\afterItemSpace%
Concerning several ideas, the Twelf system is an ancestor of the \mmt system.
Hence, it is plausible that any method given in Twelf to prove SN of STLC can be carried over to \mmt.
\end{itemize}
\item Details of the mentioned Church to Curry idea: \cite[ch.~7]{Roux:spdo20}\\[0.75em]
\afterItemSpace%
This concrete exposition of mine gives a logical relation-free account of the Church to Curry idea for the \mmt system.
A version with logical relations in mind has been implemented as of January 2021, but not yet reported on.
\end{itemize}
\printbibliography
\end{frame}