% Beamer comes with a number of default layout themes which change the colors and layouts of slides. Below is a list of all themes available, uncomment each in turn to see what they look like.
% Beamer comes with a number of color themes that can be applied to any layout theme to change its colors. Uncomment each of these in turn to see how they change the colors of your selected layout theme.
% Beamer comes with several font themes to easily change the fonts used in various parts of the presentation. Review the comments beside each one to decide if you would like to use it. Note that additional options can be specified for several of these font themes, consult the beamer documentation for more information.
\usefonttheme{default}% Typeset using the default sans serif font
%\usefonttheme{serif} % Typeset using the default serif font (make sure a sans font isn't being set as the default font if you use this option!)
%\usefonttheme{structurebold} % Typeset important structure text (titles, headlines, footlines, sidebar, etc) in bold
%\usefonttheme{structureitalicserif} % Typeset important structure text (titles, headlines, footlines, sidebar, etc) in italic serif
%\usefonttheme{structuresmallcapsserif} % Typeset important structure text (titles, headlines, footlines, sidebar, etc) in small caps serif
%------------------------------------------------
%\usepackage{mathptmx} % Use the Times font for serif text
\usepackage{palatino}% Use the Palatino font for serif text
%\usepackage{helvet} % Use the Helvetica font for sans serif text
\usepackage[default]{opensans}% Use the Open Sans font for sans serif text
%\usepackage[default]{FiraSans} % Use the Fira Sans font for sans serif text
%\usepackage[default]{lato} % Use the Lato font for sans serif text
% Inner themes change the styling of internal slide elements, for example: bullet points, blocks, bibliography entries, title pages, theorems, etc. Uncomment each theme in turn to see what changes it makes to your presentation.
% Outer themes change the overall layout of slides, such as: header and footer lines, sidebars and slide titles. Uncomment each theme in turn to see what changes it makes to your presentation.
%\useoutertheme{default}
%\useoutertheme{infolines}
%\useoutertheme{miniframes}
%\useoutertheme{smoothbars}
%\useoutertheme{sidebar}
%\useoutertheme{split}
%\useoutertheme{shadow}
%\useoutertheme{tree}
%\useoutertheme{smoothtree}
%\setbeamertemplate{footline} % Uncomment this line to remove the footer line in all slides
%\setbeamertemplate{footline}[page number] % Uncomment this line to replace the footer line in all slides with a simple slide count
%\setbeamertemplate{navigation symbols}{} % Uncomment this line to remove the navigation symbols from the bottom of all slides
\title[SGDT + GTT]{Synthetic Guarded Domain Theory + \\ Gradual Typing}% The short title in the optional parameter appears at the bottom of every slide, the full title in the main parameter is only on the title page
% \subtitle{Optional Subtitle} % Presentation subtitle, remove this command if a subtitle isn't required
\author[Eric Giovannini and Max New]{Eric Giovannini and Max New}% Presenter name(s), the optional parameter can contain a shortened version to appear on the bottom of every slide, while the main parameter will appear on the title slide
%\institute[U-M]{University of Michigan \\ \smallskip \textit{james@LaTeXTemplates.com}}
\institute[U-M]{University of Michigan}
% Your institution, the optional parameter can be used for the institution shorthand and will appear on the bottom of every slide after author names, while the required parameter is used on the title slide and can include your email address or additional information on separate lines
\date[\today]{MPLSE Reading Group \\\today}% Presentation date or conference/meeting name, the optional parameter can contain a shortened version to appear on the bottom of every slide, while the required parameter value is output to the title slide
% The table of contents outputs the sections and subsections that appear in your presentation, specified with the standard \section and \subsection commands. You may either display all sections and subsections on one slide with \tableofcontents, or display each section at a time on subsequent slides with \tableofcontents[pausesections]. The latter is useful if you want to step through each section and mention what you will discuss.
\begin{frame}
\frametitle{Overview}% Slide title, remove this command for no title
\tableofcontents% Output the table of contents (all sections on one slide)
%\tableofcontents[pausesections] % Output the table of contents (break sections up across separate slides)
Datatype that represents computations that at each step can return a value ($\eta$), terminate with an error ($\mho$), or
``think'', i.e., defer the result to a later step ($\theta$).
\begin{definition}[Lift Monad]
\begin{align*}
\li A &:= \\
&\eta\colon A \to\li A \\
&\mho\colon\li A \\
&\theta\colon\later (\li A) \to\li A
\end{align*}
\end{definition}
There is a computation $\fix(\theta)$ of type $\li A$; this represents a computation
that thinks forever and never returns a value.
\medskip
Notation: We define $\delta\colon\li A \to\li A$ by $\delta=\theta\circ\nxt$
\end{frame}
\begin{frame}
\frametitle{Predomains and Monotone Functions}
A \textbf{predomain}$A$ consists of a type (which we denote $\ty{A}$) and a relation
$\le_A$ on $A$ that satisfies the axioms of a partial ordering.
\smallskip
Since our types have an underlying order structure (representing the error ordering),
we want to model types as partially-ordered sets in the semantics.
\bigskip
Then functions between terms will be modeled as \emph{monotone} functions between
their corresponding predomains.
\smallskip
We write $f \colon A \monto B$ to indicate that $f$ is a monotone
function from $A$ to $B$, i.e, for all $a_1\le_A a_2$, we have $f(a_1)\le_B f(a_2)$.
\end{frame}
\begin{frame}
\frametitle{Predomains}
We define predomains for natural numbers, the dynamic type (which we denote $D$), and for monotone functions between predomains (which we denote $A_i \To A_o$).
\medskip
For Dyn, the underlying type is defined to be
\[\ty{D}=\mathbb{N}\,\,+\later(D \monto D)\]
This definition is valid because the occurrences of $D$ are guarded by the $\later$.
The ordering is defined via guarded recursion by cases on the argument.
\medskip
We also define a predomain for the ``lifting'' of a predomain by the $\li$ monad.
We denote this by $\li A$.
\end{frame}
\begin{frame}
\frametitle{Lock-Step Ordering and Weak Bisimilarity}
For a predomain $A$, the ordering on $\li A$ is called the ``lock-step error ordering'', denoted $l \ltls l'$.
Intuitively: $l$ is less than $l'$ if they are in lock-step with regard to their
intensional behavior, up to $l$ erroring.
\begin{itemize}
\item$\eta\, x \ltls\eta\, y$ if $x \le_A y$.
\item$\mho\ltls l$ for all $l$
\item$\theta\,\tilde{r}\ltls\theta\,\tilde{r'}$ if
$\later_t (\tilde{r}_t \ltls\tilde{r'}_t)$
\end{itemize}
We analogously define a lifting of a heterogeneous relation $R$ between $A$ and $B$
to a relation $L(R)$ between $\li A$ and $\li B$.
\end{frame}
\begin{frame}
\frametitle{Lock-Step Ordering and Weak Bisimilarity}
We also define another ordering on $\li A$, called ``weak bisimilarity'',
written $l \bisim l'$.
We say $l \bisim l'$ if they are equivalent ``up to delays''.
\begin{align*}
&\mho\bisim\mho\\
%
&\eta\, x \bisim\eta\, y \text{ if }
x \sim_A y \\
%
&\theta\,\tilde{x}\bisim\theta\,\tilde{y}\text{ if }
\later_t (\tilde{x}_t \bisim\tilde{y}_t) \\
%
&\theta\,\tilde{x}\bisim\mho\text{ if }
\theta\,\tilde{x} = \delta^n(\mho) \text{ for some $n$}\\
%
&\theta\,\tilde{x}\bisim\eta\, y \text{ if }
(\theta\,\tilde{x} = \delta^n(\eta\, x))
\text{ for some $n$ and $x : \ty{A}$ such that $x \sim_A y$}\\
%
&\mho\bisim\theta\,\tilde{y}\text{ if }
\theta\,\tilde{y} = \delta^n(\mho) \text{ for some $n$}\\
%
&\eta\, x \bisim\theta\,\tilde{y}\text{ if }
(\theta\,\tilde{y} = \delta^n (\eta\, y))
\text{ for some $n$ and $y : \ty{A}$ such that $x \sim_A y$}
\end{align*}
\end{frame}
\begin{frame}
\frametitle{EP Pairs}
We will model casts as \emph{EP-pairs}.
\bigskip
Given predomains $A$ and $B$, an EP-pair $c : A \ep B$ consists of $\emb{c}{\cdot}\colon A \to B$ and $\proj{c}{\cdot}\colon B \to\li A$, and a monotone relation $R_c$ between $A$ and $B$.
\medskip
The relation $R_c$ should be related in a specific way to the embedding and projection functions.
\end{frame}
\begin{frame}
\frametitle{EP Pairs}
We have an identity EP-pair $\id : A \ep A$, with the embedding and projection equal to the identity and $\eta$, respectively.
% We want to prove that the lock-step and weak bisimilarity relations
% are \emph{adequate}, i.e.,
% \end{frame}
\section{Discussion and Lessons Learned}
\frame{\tableofcontents[currentsection]}
\begin{frame}
\frametitle{Benefits and Drawbacks}
Positives:
\begin{itemize}
\item SGDT handles much of the tedious step-index reasoning
\item Clarifies the underlying semantic and algebraic structure
\end{itemize}
Drawbacks:
\begin{itemize}
\item Intensional semantics is much more complicated (needed to introduce wait functions)
\item Still need to work ``analytically'' with monotone functions
\item Need to do a lot of manual ``unfolding'' of fixpoint definitions in Guarded Cubical Agda
\end{itemize}
\end{frame}
\begin{frame}[allowframebreaks] % Use [allowframebreaks] to allow automatic splitting across slides if the content is too long
\frametitle{References}
\begin{thebibliography}{99}% Beamer does not support BibTeX so references must be inserted manually as below, you may need to use multiple columns and/or reduce the font size further if you have many references
\footnotesize% Reduce the font size in the bibliography
\bibitem[1]{AM2013}
Robert Atkey and Conor McBride.
\newblock Productive coprogramming with guarded recursion.
Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland
\newblock Refined Criteria for Gradual Typing
\newblock\emph{1st Summit on Advances in Programming Languages (SNAPL 2015). }
\end{thebibliography}
\end{frame}
\begin{comment}
\section{Text Examples}% Sections are added in order to organize your presentation into discrete blocks, all sections and subsections are automatically output to the table of contents as an overview of the talk but NOT output in the presentation as separate slides
%------------------------------------------------
\subsection{Paragraphs and Lists}
\begin{frame}
\frametitle{Paragraphs of Text}
Sed iaculis \alert{dapibus gravida}. Morbi sed tortor erat, nec interdum arcu. Sed id lorem lectus. Quisque viverra augue id sem ornare non aliquam nibh tristique. Aenean in ligula nisl. Nulla sed tellus ipsum. Donec vestibulum ligula non lorem vulputate fermentum accumsan neque mollis.
\bigskip% Vertical whitespace
% Quote example
\begin{quote}
Sed diam enim, sagittis nec condimentum sit amet, ullamcorper sit amet libero. Aliquam vel dui orci, a porta odio.\\
--- Someone, somewhere\ldots
\end{quote}
\bigskip% Vertical whitespace
Nullam id suscipit ipsum. Aenean lobortis commodo sem, ut commodo leo gravida vitae. Pellentesque vehicula ante iaculis arcu pretium rutrum eget sit amet purus. Integer ornare nulla quis neque ultrices lobortis.
\end{frame}
%------------------------------------------------
\begin{frame}
\frametitle{Lists}
\framesubtitle{Bullet Points and Numbered Lists}% Optional subtitle
\begin{itemize}
\item Lorem ipsum dolor sit amet, consectetur adipiscing elit
\item Aliquam blandit faucibus nisi, sit amet dapibus enim tempus
\begin{itemize}
\item Lorem ipsum dolor sit amet, consectetur adipiscing elit
\item Nam cursus est eget velit posuere pellentesque
\end{itemize}
\item Nulla commodo, erat quis gravida posuere, elit lacus lobortis est, quis porttitor odio mauris at libero
\end{itemize}
\bigskip% Vertical whitespace
\begin{enumerate}
\item Nam cursus est eget velit posuere pellentesque
\item Vestibulum faucibus velit a augue condimentum quis convallis nulla gravida
\end{enumerate}
\end{frame}
%------------------------------------------------
\subsection{Blocks}
\begin{frame}
\frametitle{Blocks of Highlighted Text}
\begin{block}{Block Title}
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Integer lectus nisl, ultricies in feugiat rutrum, porttitor sit amet augue.
\end{block}
\begin{exampleblock}{Example Block Title}
Aliquam ut tortor mauris. Sed volutpat ante purus, quis accumsan.
\end{exampleblock}
\begin{alertblock}{Alert Block Title}
Pellentesque sed tellus purus. Class aptent taciti sociosqu ad litora torquent per conubia nostra, per inceptos himenaeos.
\end{alertblock}
\begin{block}{}% Block without title
Suspendisse tincidunt sagittis gravida. Curabitur condimentum, enim sed venenatis rutrum, ipsum neque consectetur orci.
\end{block}
\end{frame}
%------------------------------------------------
\subsection{Columns}
\begin{frame}
\frametitle{Multiple Columns}
\framesubtitle{Subtitle}% Optional subtitle
\begin{columns}[c] % The "c" option specifies centered vertical alignment while the "t" option is used for top vertical alignment
\begin{column}{0.45\textwidth}% Left column width
\textbf{Heading}
\begin{enumerate}
\item Statement
\item Explanation
\item Example
\end{enumerate}
\end{column}
\begin{column}{0.5\textwidth}% Right column width
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Integer lectus nisl, ultricies in feugiat rutrum, porttitor sit amet augue. Aliquam ut tortor mauris. Sed volutpat ante purus, quis accumsan dolor.
\begin{frame}[fragile] % Need to use the fragile option when verbatim is used in the slide
\frametitle{Verbatim}
\begin{example}[Theorem Slide Code]
\begin{verbatim}
\begin{frame}
\frametitle{Theorem}
\begin{theorem}[Mass--energy equivalence]
$E = mc^2$
\end{theorem}
\end{frame}\end{verbatim}% Must be on the same line
\end{example}
\end{frame}
%------------------------------------------------
\begin{frame}
Slide without title.
\end{frame}
%------------------------------------------------
\section{Referencing}
\begin{frame}
\frametitle{Citing References}
An example of the \texttt{\textbackslash cite} command to cite within the presentation:
\bigskip% Vertical whitespace
This statement requires citation \cite{p1,p2}.
\end{frame}
%------------------------------------------------
\begin{frame}% Use [allowframebreaks] to allow automatic splitting across slides if the content is too long
\frametitle{References}
\begin{thebibliography}{99}% Beamer does not support BibTeX so references must be inserted manually as below, you may need to use multiple columns and/or reduce the font size further if you have many references
\footnotesize% Reduce the font size in the bibliography
