diff --git a/beamer/lc-beamer/Makefile b/beamer/lc-beamer/Makefile new file mode 100644 index 0000000..af09ed1 --- /dev/null +++ b/beamer/lc-beamer/Makefile @@ -0,0 +1,41 @@ +PACKAGE_STY = $(wildcard *.sty) +PACKAGE_IMG = $(wildcard ccc_img/*) + +DESTDIR ?= $(shell kpsewhich -var-value=TEXMFHOME) +INSTALL_DIR = $(DESTDIR)/tex/latex/ccc + +EXAMPLE_SRC = example.tex +EXAMPLE_PDF = example.pdf + +CACHE_DIR := $(shell pwd)/.latex-cache + +COMPILE_TEX := latexmk -lualatex -output-directory="$(CACHE_DIR)" + +.PHONY: install uninstall example all clean + +all: example + +example: $(EXAMPLE_PDF) + +install: $(PACKAGE_STY) + @mkdir -p "$(INSTALL_DIR)" + @cp $(PACKAGE_STY) "$(INSTALL_DIR)" + @mkdir -p "$(INSTALL_DIR)/ccc_img" + @cp $(PACKAGE_IMG) "$(INSTALL_DIR)/ccc_img" + +uninstall: + @rm -f $(addprefix "$(INSTALL_DIR)"/, $(PACKAGE_STY)) + @rm -f $(addprefix "$(INSTALL_DIR)"/, $(PACKAGE_IMG)) + @rmdir "$(INSTALL_DIR)/ccc_img" + @rmdir "$(INSTALL_DIR)" + +clean: + @rm -rf "$(CACHE_DIR)" + @rm -f "$(EXAMPLE_PDF)" + +$(EXAMPLE_PDF) : $(EXAMPLE_SRC) + @$(COMPILE_TEX) $(EXAMPLE_SRC) + @cp "$(CACHE_DIR)/$(EXAMPLE_PDF)" . + + + diff --git a/beamer/lc-beamer/beamercolorthemeccc.sty b/beamer/lc-beamer/beamercolorthemeccc.sty new file mode 100644 index 0000000..5b6ab48 --- /dev/null +++ b/beamer/lc-beamer/beamercolorthemeccc.sty @@ -0,0 +1,31 @@ +\mode + +\definecolor{darkblue}{HTML}{265E87} +\definecolor{darkteal}{RGB}{0,180,141} +\definecolor{orange}{RGB}{231,123,20} +\definecolor{gray}{rgb}{0.929,0.929,0.929} + +% Settings +\setbeamercolor*{title page header}{fg=darkblue} +\setbeamercolor*{author}{fg=darkblue} +\setbeamercolor*{institute}{fg=darkblue} +\setbeamercolor*{date}{fg=darkblue} +\setbeamercolor*{frametitle}{fg=darkblue} +\setbeamercolor*{framesubtitle}{fg=darkblue} +\setbeamercolor*{pagenum}{fg=darkblue} +\setbeamercolor*{alerted text}{fg=orange} +\setbeamercolor*{item}{fg=darkblue} +\setbeamercolor*{subitem}{fg=darkteal} +\setbeamercolor*{subsubitem}{fg=orange} +\setbeamercolor*{block title}{fg=darkblue} +\setbeamercolor*{block title alerted}{fg=orange} +\setbeamercolor*{block title example}{fg=darkteal} +\setbeamercolor*{block body}{fg=black} +\setbeamercolor*{bibliography entry title}{fg=black} +\setbeamercolor*{bibliography entry author}{fg=darkblue} +\setbeamercolor*{bibliography entry location}{fg=black} +\setbeamercolor*{bibliography entry note}{fg=black} +\setbeamercolor*{section in toc}{fg=darkblue} +\setbeamercolor*{subsection in toc}{fg=darkteal} + +\mode diff --git a/beamer/lc-beamer/beamerfontthemeccc.sty b/beamer/lc-beamer/beamerfontthemeccc.sty new file mode 100644 index 0000000..775d79d --- /dev/null +++ b/beamer/lc-beamer/beamerfontthemeccc.sty @@ -0,0 +1,11 @@ +\mode + +\setbeamerfont{title}{size=\Large,series=\bfseries} +\setbeamerfont{subtitle}{series=\bfseries} +\setbeamerfont{frametitle}{size=\large, series=\bfseries} +\setbeamerfont{framesubtitle}{size=\small, series=\bfseries} +\setbeamerfont{pagenum}{size=\footnotesize} +\setbeamerfont{block body}{size=\normalsize} +\setbeamerfont{footnote}{size=\scriptsize} + +\mode diff --git a/beamer/lc-beamer/beamerinnerthemeccc.sty b/beamer/lc-beamer/beamerinnerthemeccc.sty new file mode 100644 index 0000000..be08d41 --- /dev/null +++ b/beamer/lc-beamer/beamerinnerthemeccc.sty @@ -0,0 +1,182 @@ +\mode + +\def\beamer@andinst{\\[0.5em]} + +\setbeamertemplate{background}{ + \begin{tikzpicture} + \useasboundingbox (0,0) rectangle(\the\paperwidth,\the\paperheight); + % the header + \fill[gray, anchor=north west] (0,\the\paperheight) rectangle(\the\paperwidth,\paperheight-1.4cm); + % ccc logo on the left (only on title page) + \ifnum\thepage=1\relax% + \node[anchor=west, inner sep=0] (header) at (0.25cm,\paperheight-0.7cm) { + \includegraphics[width=90px]{ccc_img/cclogo.pdf}}; + \fi + % cfaed logo on the right (only on title page or if cfaedlogo is set) + \ifbeamer@cfaedlogo + \node[anchor=east, inner sep=0] (header) at (\paperwidth-0.25cm,\paperheight-0.7cm) { + \includegraphics[width=60px]{ccc_img/cfaed.png}}; + \else + \ifnum\thepage=1\relax% + \node[anchor=east, inner sep=0] (header) at (\paperwidth-0.25cm,\paperheight-0.7cm) { + \includegraphics[width=60px]{ccc_img/cfaed.png}}; + \fi + \fi + % the footer + \node[anchor=south west, inner sep=0] (footer) at (0,0) { + \ifnum\thepage=1\relax% + \includegraphics[width=\paperwidth]{ccc_img/titlefooter.png} + \fi + \includegraphics[width=\paperwidth]{ccc_img/footer.png}}; + \ifnum\thepage>1\relax% + % page number on the left + \node[anchor=west, inner sep=0] (pagenum) at (0.2,0.55) { + \usebeamerfont{pagenum}\usebeamercolor[fg]{pagenum}\insertframenumber}; + % page ccc logo on the right + \ifbeamer@ccclogo + \node[anchor=east, inner sep=0] (pagenum) at (\pagewidth-0.2,0.55) { + \includegraphics[width=50pt]{ccc_img/cclogo.pdf}}; + \fi + \fi + \end{tikzpicture} +} + +\defbeamertemplate*{title page}{ccc}[1][]{ + \vskip1cm% + \begin{beamercolorbox}[wd=\textwidth,#1]{title page header} + \usebeamerfont{title}\inserttitle\par% + \medskip + \usebeamerfont{subtitle}\insertsubtitle\par% + \end{beamercolorbox}% + \vskip0.5cm% + \begin{beamercolorbox}[wd=\textwidth,#1]{author} + \usebeamerfont{author}\insertauthor% + \end{beamercolorbox} + \vskip0.5cm% + \begin{beamercolorbox}[wd=\textwidth,#1]{institute} + \usebeamerfont{institute}\insertinstitute% + \end{beamercolorbox} + \vskip0.5cm% + \begin{beamercolorbox}[wd=\textwidth,#1]{date} + \usebeamerfont{date}\insertdate% + \end{beamercolorbox} + \vfill +} + +% Frame title +\defbeamertemplate*{frametitle}{ccc}[1][] +{ + \begin{tikzpicture} + \useasboundingbox (0,0) rectangle(\textwidth,1.4cm); + \ifx\insertframesubtitle\@empty% + \node[anchor=west, inner sep=0, text width=\textwidth, align=left] at (0,0.7){ + \usebeamerfont{frametitle}\insertframetitle}; + \else + \node[anchor=west, inner sep=0, text width=\textwidth, align=left] at (0,0.7){ + \usebeamerfont{frametitle}\insertframetitle\\ + \usebeamerfont{framesubtitle}\insertframesubtitle}; + \fi + \end{tikzpicture} +} + +\defbeamertemplate*{block begin}{ccc} +{ + \par\vskip\medskipamount% + \usebeamercolor{block title} + \begin{tikzpicture} + \node [ + draw=fg, inner sep=1ex, + text width=\textwidth-2ex-1pt, + minimum width=\textwidth-1pt, + rounded corners + ] (BOXCONTENT) \bgroup% + \ifx\insertblocktitle\@empty\else\par\fi + \usebeamerfont{block body} + \usebeamercolor[fg]{block body} +} + +\defbeamertemplate*{block end}{ccc} +{ + \egroup; + \usebeamercolor{block title} + \ifx\insertblocktitle\@empty + \else{ + \node[ fill=bg, anchor=west, text=fg, rounded corners ] at + ([shift={(5pt,0)}]BOXCONTENT.north west) {\insertblocktitle}; + } + \fi + \end{tikzpicture} + \vskip\smallskipamount +} + +\defbeamertemplate*{block example begin}{ccc} +{ + \par\vskip\medskipamount% + \usebeamercolor{block title example} + \begin{tikzpicture} + \node [ + draw=fg, inner sep=1ex, + text width=\textwidth-2ex-1pt, + minimum width=\textwidth-1pt, + rounded corners + ] (BOXCONTENT) \bgroup% + \ifx\insertblocktitle\@empty\else\par\fi + \usebeamerfont{block body} + \usebeamercolor[fg]{block body} +} + +\defbeamertemplate*{block example end}{ccc} +{ + \egroup; + \usebeamercolor{block title example} + \ifx\insertblocktitle\@empty + \else% + { + \node [ fill=bg, anchor=west, text=fg, rounded corners] + at ([shift={(5pt,0)}]BOXCONTENT.north west) {\insertblocktitle}; + } + \fi + \end{tikzpicture} + \vskip\smallskipamount +} + +\defbeamertemplate*{block alerted begin}{ccc} +{ + \par\vskip\medskipamount% + \usebeamercolor{block title alerted} + \begin{tikzpicture} + \node [ + draw=fg, inner sep=1ex, + text width=\textwidth-2ex-1pt, + minimum width=\textwidth-1pt, + rounded corners + ] (BOXCONTENT) \bgroup% + \ifx\insertblocktitle\@empty\else\par\fi + \usebeamerfont{block body} + \usebeamercolor[fg]{block body} +} + +\defbeamertemplate*{block alerted end}{ccc} +{ + \egroup; + \usebeamercolor{block title alerted} + \ifx\insertblocktitle\@empty + \else% + { + \node [fill=bg, anchor=west, text=fg, rounded corners] at + ([shift={(5pt,0)}]BOXCONTENT.north west) {\insertblocktitle}; + } + \fi + \end{tikzpicture} + \vskip\smallskipamount +} + +% Items +\setbeamertemplate{itemize items}{\Squarepipe} + +\setbeamertemplate{footline}{\vspace{4mm}} + +\setbeamertemplate{section in toc}[sections numbered] +\setbeamertemplate{subsection in toc}[subsections numbered] + +\mode diff --git a/beamer/lc-beamer/beamerouterthemeccc.sty b/beamer/lc-beamer/beamerouterthemeccc.sty new file mode 100644 index 0000000..e69de29 diff --git a/beamer/lc-beamer/beamerthemeccc.sty b/beamer/lc-beamer/beamerthemeccc.sty new file mode 100644 index 0000000..cf657ef --- /dev/null +++ b/beamer/lc-beamer/beamerthemeccc.sty @@ -0,0 +1,31 @@ +\newif\ifbeamer@cfaedlogo +\beamer@cfaedlogofalse +\DeclareOptionBeamer{cfaedlogo}{\beamer@cfaedlogotrue} +\ProcessOptionsBeamer + +\newif\ifbeamer@ccclogo +\beamer@ccclogotrue +\DeclareOptionBeamer{noccclogo}{\beamer@ccclogofalse} +\ProcessOptionsBeamer + +\mode + +% Requirement +\RequirePackage{tikz} +\usetikzlibrary{calc} +\RequirePackage{fontspec} +\RequirePackage{marvosym} + +% Settings +\useinnertheme{ccc} +\useoutertheme{ccc} +\usecolortheme{ccc} +\usefonttheme{ccc} + +% Set the font +\setsansfont{Open Sans} + +% disable navigation symbols +\setbeamertemplate{navigation symbols}{} + +\mode diff --git a/beamer/lc-beamer/ccc_img/cfaed.png b/beamer/lc-beamer/ccc_img/cfaed.png new file mode 100755 index 0000000..6c7a524 Binary files /dev/null and b/beamer/lc-beamer/ccc_img/cfaed.png differ diff --git a/beamer/lc-beamer/ccc_img/footer.png b/beamer/lc-beamer/ccc_img/footer.png new file mode 100755 index 0000000..54f4f92 Binary files /dev/null and b/beamer/lc-beamer/ccc_img/footer.png differ diff --git a/beamer/lc-beamer/ccc_img/header.png b/beamer/lc-beamer/ccc_img/header.png new file mode 100755 index 0000000..cc7122b Binary files /dev/null and b/beamer/lc-beamer/ccc_img/header.png differ diff --git a/beamer/lc-beamer/ccc_img/titlefooter.png b/beamer/lc-beamer/ccc_img/titlefooter.png new file mode 100644 index 0000000..6f0300b Binary files /dev/null and b/beamer/lc-beamer/ccc_img/titlefooter.png differ diff --git a/beamer/lc-beamer/example.tex b/beamer/lc-beamer/example.tex new file mode 100644 index 0000000..c6aa7ae --- /dev/null +++ b/beamer/lc-beamer/example.tex @@ -0,0 +1,454 @@ +\documentclass{beamer} + + +\usepackage[utf8]{inputenc} +\usepackage{formal-grammar} +\usepackage[dvipsnames]{xcolor} +\usepackage{mathpartir} +\usepackage{stmaryrd} + +\newcommand{\metavariable}[1]{\textcolor{teal}{#1}} +\newcommand{\typeterminal}[1]{\textcolor{brown}{#1}} +\newcommand{\exprterminal}[1]{\textcolor{Sepia}{#1}} + + + +\title{A functional core calculus with ladder-types} +%\date[ISPN ’80]{27th International Symposium of Prime Numbers} + + +\author[Euclid]{Michael Sippel \texttt{michael.sippel@mailbox.tu-dresden.de}\inst{1}} +\institute{\inst{1} Technische Universität Dresden} + +\usetheme{ccc} + +\begin{document} + +\begin{frame} +\titlepage +\end{frame} + +\begin{frame} + \frametitle{Type Systems} + \framesubtitle{Tension between Safety and Flexibility} + + \begin{itemize} + \item<1-> Goal: eliminate undefined behaviour, + facilitate abstract code + \item<2-> simple types are overly restrictive, + loss of low level control + + \item<3-|alert@3> polymorphism + (regain flexibility in type-safe way) + \begin{itemize} + \item<4-> parametric polymorphism (generics) + \item<4-> subtype polymorphism (inheritance / coercions) + \end{itemize} + \end{itemize} +\end{frame} + +\begin{frame}{How to get fast code?} + \framesubtitle{Requirements for a type system} + \begin{itemize} + \item<1-> algorithmic optimization + \begin{itemize} + \item see which methods are used most frequently + \item switch structures to reduce complexity there + \item identify special cases + \end{itemize} + + \item<2-> optimize implementation detail: + \begin{itemize} + \item remove indirection + \item bottleneck? memory!\\ + (plenty of Main-memory, but FAST memory is scarce\\ + \(\rightarrow\) improve cache \& bus efficiency with compact representations) + + \begin{itemize} + \item<3-> Balance De-/Encode Overhead + vs. Fetch-Overhead + + \item<4-> Synchronize locality in access order and memory layout. + -> elements accessed in succession shall be close in memory. + (e.g. AoS vs SoA) + + \item<5-> accounting for machine specific cache-sizes + \item<6-> accounting for SIMD instructions + \item<7-> interfacing with kernels running on accelerator devices + \end{itemize} + \end{itemize} + \end{itemize} +\end{frame} + +\begin{frame}{Abstract Concept - Multiple Representations} +\framesubtitle{Requirements for a type system} + \begin{itemize} + \item + \end{itemize} +\end{frame} + +\begin{frame}{Coercions: (In-)Coherence with Transitivity} + \begin{itemize} + \item<1-> Common example: coerce \texttt{Int -> Real} + (subsumption \(\mathbb{N} \subset \mathbb{R}\)) + + \begin{itemize} + \item \texttt{Int -> Real} + \item \texttt{Int -> String} + \item \texttt{Real -> String} + \end{itemize} + + \item<2-> transitivity creates two extensionally \emph{different} coercion paths: + \begin{itemize} + \item \texttt{Int -> String} (3 -> "3") + \item \texttt{Int -> Real -> String} (3 -> "3.0") + \end{itemize} + + \item<3-> Subsumptive interpretation is misleading! + \item<3-> \texttt{Int -> Real} is not as unambiguous as it might seem. + \begin{itemize} + \item value ranges (e.g. map int to unit interval [0,1]) + \item multiple quantization functions (linear, exponential, \dots) + \end{itemize} + + \end{itemize} +\end{frame} + +\begin{frame}{Sea of Types} +\includegraphics[width=\textwidth]{sot-int.png} +\end{frame} + +\begin{frame}{Sea of Types} +\includegraphics[width=\textwidth]{sot-json.png} +\end{frame} + + +\begin{frame}{Ladder Types} + \begin{block}{Intuition} + Encode "represented-as" relation into type terms + \end{block} + + \begin{block}{} + \( \tau_1 \sim \tau_2 \) reads "\(\tau_1\) represented as \(\tau_2\)" + \end{block} + + \begin{example}\( + Color \sim sRGB + \sim HSV \sim \langle \text{Vec3} \quad \mathbb{R}_{[0,1]} + \sim \langle \text{QuantizeLinear} \quad 256 \rangle + \sim \mathbb{Z}_{256} \sim \text{machine.UInt8} \sim \text{Byte} + \rangle + \sim \text{[Byte; 3]} + \)\end{example} +\end{frame} + +\begin{frame}{Extending System F} +\small +\begin{grammar} + +\firstcase{ T }{ + \metavariable{\sigma} +}{Base Type} + +\otherform{ + \metavariable{\alpha} +}{Type Variable} + +\otherform{ + \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \nonterm{T} +}{Universal Type} + +\otherform{ + \typeterminal{<} \nonterm{T} \quad \nonterm{T} \typeterminal{>} +}{Specialized Type} + +\otherform{ + \nonterm{T} \quad \typeterminal{\rightarrow} \quad \nonterm{T} +}{Function Type} + +\otherform{ + \nonterm{T} \quad \typeterminal{\rightarrow_\text{morph}} \quad \nonterm{T} +}{Morphism Type} + +\otherform{ + \nonterm{T} \quad \typeterminal{\sim} \quad \nonterm{T} +}{Ladder Type} + +$$\\$$ + +\firstcase{ E +% T_\selexpr +} + { \metavariable{x} +} {Variable} + +\otherform{ + \exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad + \nonterm{ E } + \quad \exprterminal{in} \quad + \nonterm{ E } +}{Variable Binding} + +\otherform{ + $$ \exprterminal{\Lambda} \metavariable{\alpha} + \quad \exprterminal{\mapsto} \quad $$ + \nonterm{ E } +}{Type Abstraction} + +\otherform{ + $$ \exprterminal{\lambda} \metavariable{x} $$ + \exprterminal{:} \nonterm{ T } + \quad $$\exprterminal{\mapsto}$$ \quad + \nonterm{ E } +}{Value Abstraction} + +\otherform{ + $$ \exprterminal{\lambda} \metavariable{x} $$ + \exprterminal{:} \nonterm{ T } + \quad $$\exprterminal{\mapsto_\text{morph}}$$ \quad + \nonterm{ E } +}{Value Morphism} + +\otherform{ + \nonterm{ E } + \quad + \nonterm{ T } +}{Type Application} + +\otherform{ + \nonterm{ E } + \quad + \nonterm{ E } +}{Value Application} + +\otherform{ + \nonterm{ E } + \quad + \exprterminal{as} + \quad + \nonterm{ T } +}{Ascension} + +\otherform{ + \nonterm{ E } + \quad + \exprterminal{des} + \quad + \nonterm{ T } +}{Descension} + +\end{grammar} + + +\end{frame} + +\begin{frame}{Morphism Graph} + +\begin{definition}[Morphism Paths] +\label{def:pathrules} +\begin{mathpar} + + \inferrule[M-Sub]{ + \metavariable{\tau} \leq \metavariable{\tau'} + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + } + + \inferrule[M-Single]{ + (\metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}) \in \Gamma + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + } + + \inferrule[M-Chain]{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\\ + \Gamma \vdash \metavariable{\tau'} \leadsto \metavariable{\tau''} + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau''} + } + + \inferrule[M-MapSeq]{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + }{ + \Gamma \vdash + \typeterminal{\langle\text{Seq } \metavariable{\tau}\rangle} \leadsto + \typeterminal{\langle\text{Seq } \metavariable{\tau'}\rangle} + } +\end{mathpar} +\end{definition} +\end{frame} + +\begin{frame}{Morphism Graph} + +\begin{example}[Morphism Graph] +\begin{mathpar} +\small +\text{Assume } +\Gamma := \{\\ + \exprterminal{\text{degrees-to-turns}} : \typeterminal{\text{Angle}\sim\text{Degrees}\sim\mathbb{R} \quad \rightarrow_\text{morph} \quad \text{Angle}\sim\text{Turns}\sim\mathbb{R}},\\ + \exprterminal{\text{turns-to-radians}} : \typeterminal{\text{Angle}\sim\text{Turns}\sim\mathbb{R} \quad \rightarrow_\text{morph} \quad \text{Angle}\sim\text{Radians}\sim\mathbb{R}},\\ +\}. +\end{mathpar} +\end{example} + +\end{frame} + + +\begin{frame}{Morphism Graph} + +\begin{example}[Morphism Graph] +Then .. +\small +\begin{itemize} +\item \(\Gamma \vdash \typeterminal{\text{Angle}\sim\text{Degrees}\sim\mathbb{R}} \leadsto \typeterminal{\mathbb{R}}\) (by \textsc{M-Sub}) +\item \(\Gamma \vdash \typeterminal{\text{Angle}\sim\text{Degrees}\sim\mathbb{R}} \leadsto \typeterminal{\text{Angle}\sim\text{Radians}\sim\mathbb{R}}\) (by \textsc{M-Chain}) +\item \(\Gamma \vdash \typeterminal{\langle\text{Seq }\text{Angle}\sim\text{Degrees}\sim\mathbb{R}\rangle} \leadsto \typeterminal{\langle\text{Seq }\text{Angle}\sim\text{Radians}\sim\mathbb{R}\rangle}\) (by \textsc{M-MapSeq}) +\end{itemize} +\end{example} + +\end{frame} + +\begin{frame}{Typing} + +\begin{definition}[Typing Relation] +\begin{mathpar} + \inferrule[T-App]{ + \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ + \Gamma \vdash \metavariable{a} : \metavariable{\sigma'}\\ + \Gamma \vdash \metavariable{\sigma'} \leadsto \metavariable{\sigma} + }{ + \Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau} + } +\end{mathpar} +\end{definition} +\end{frame} + +\begin{frame}{Translation} +\begin{definition}[Morphism Translation] +\begin{mathpar} +\small + +\Big{\llbracket} + \inferrule[M-Sub]{ + \metavariable{\tau} \leq \metavariable{\tau'} + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + } +\Big{\rrbracket} = \exprterminal{\lambda x:\metavariable{\tau} \mapsto x} +\and + +\Big{\llbracket} + \inferrule[M-Single]{ + (\metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}) \in \Gamma + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + } +\Big{\rrbracket} = \metavariable{h} +\and + +\end{mathpar} +\end{definition} +\end{frame} + +\begin{frame}{Translation} +\begin{definition}[Morphism Translation (2)] +\begin{mathpar} +\small +\Big{\llbracket} + \inferrule[M-Chain]{ + C_1 :: \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\\ + C_2 :: \Gamma \vdash \metavariable{\tau'} \leadsto \metavariable{\tau''} + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau''} + } +\Big{\rrbracket} = \exprterminal{\lambda \text{x}:\metavariable{\tau} \mapsto} + \Big{\llbracket} C_2 \Big{\rrbracket} + \exprterminal{(}\Big{\llbracket} C_1 \Big{\rrbracket} \exprterminal{\text{x})} +\and + + +\Big{\llbracket} + \inferrule[M-MapSeq]{ + C_1 :: \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + }{ + \Gamma \vdash + \typeterminal{\langle\text{Seq } \metavariable{\tau}\rangle} \leadsto + \typeterminal{\langle\text{Seq } \metavariable{\tau'}\rangle} + } +\Big{\rrbracket} = \exprterminal{\lambda \text{xs}:\typeterminal{\langle\text{Seq }\metavariable{\tau}\rangle} \mapsto} + \exprterminal{( \text{map}} \Big{\llbracket} C_1 \Big{\rrbracket} \exprterminal{\text{xs})} + +\end{mathpar} +\end{definition} +\end{frame} + +\begin{frame}{Translation} + +\begin{definition}[Expression Translation] +Translates a type-derivation tree into a fully expanded expression + +\begin{mathpar} +\Big{\llbracket} + \inferrule[T-App]{ + D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ + D_2 :: \Gamma \vdash \metavariable{a} : \metavariable{\sigma'}\\\\ + C :: \Gamma \vdash \metavariable{\sigma'} \leadsto \metavariable{\sigma} + }{ + \Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau} + } +\Big{\rrbracket} = + \Big{\llbracket}D_1\Big{\rrbracket} + \exprterminal{(} + \Big{\llbracket}C\Big{\rrbracket} + \Big{\llbracket}D_2\Big{\rrbracket} + \exprterminal{)} +\end{mathpar} +\end{definition} +\end{frame} + + +\begin{frame}{Soundness} + +\begin{lemma}[Morphism generation has correct type] +\begin{mathpar} +C :: \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\\ +\Rightarrow \Gamma \vdash \llbracket C \rrbracket : \metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'} +\end{mathpar} +\end{lemma} + +\begin{lemma}[Expression Translation preserves typing] +\begin{mathpar} +D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\ +\Rightarrow \Gamma \vdash \llbracket D \rrbracket : \metavariable{\tau} +\end{mathpar} +\end{lemma} +\end{frame} + +\begin{frame}{Soundness} + +\begin{theorem}[Preservation] +\begin{mathpar} \forall \Gamma, \metavariable{e}, \metavariable{\tau},\\ +D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\ +\Rightarrow \llbracket D \rrbracket \rightarrow_{eval} \metavariable{e'} \\ +\Rightarrow \Gamma \vdash \metavariable{e'} : \metavariable{\tau} +\end{mathpar} +\end{theorem} +\end{frame} + + +\begin{frame}{Soundness} +\begin{theorem}[Progress] +\begin{mathpar} \forall \Gamma, \metavariable{e}, \metavariable{\tau},\\ +D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\ +\Rightarrow \llbracket D \rrbracket \text{ is a value} \\ \vee \\ +\exists \metavariable{e'} . \llbracket D \rrbracket \rightarrow_{eval} \metavariable{e'} \\ +\end{mathpar} +\end{theorem} +\end{frame} + +\begin{frame}{Summary} +todo +\end{frame} + +\end{document} + diff --git a/beamer/lc-beamer/sot-int.png b/beamer/lc-beamer/sot-int.png new file mode 100644 index 0000000..3931e69 Binary files /dev/null and b/beamer/lc-beamer/sot-int.png differ diff --git a/beamer/lc-beamer/sot-json.png b/beamer/lc-beamer/sot-json.png new file mode 100644 index 0000000..91cee1a Binary files /dev/null and b/beamer/lc-beamer/sot-json.png differ