paper.tex

\documentclass[sigconf,anonymous,review,screen,9pt]{acmart}
\let\Bbbk\relax

\usepackage{quiver}
\usepackage{mathpartir}
% \usepackage{tikz-cd}
\usepackage{enumitem}
\usepackage{wrapfig}
\usepackage{fancyvrb}
\usepackage{comment}
\usepackage{array}


%% Rights management information.  This information is sent to you
%% when you complete the rights form.  These commands have SAMPLE
%% values in them; it is your responsibility as an author to replace
%% the commands and values with those provided to you when you
%% complete the rights form.
\setcopyright{acmcopyright}
\copyrightyear{2018}
\acmYear{2018}
\acmDOI{10.1145/1122445.1122456}

%% These commands are for a PROCEEDINGS abstract or paper.
\acmConference[Woodstock '18]{Woodstock '18: ACM Symposium on Neural
  Gaze Detection}{June 03--05, 2018}{Woodstock, NY}
\acmBooktitle{Woodstock '18: ACM Symposium on Neural Gaze Detection,
  June 03--05, 2018, Woodstock, NY}
\acmPrice{15.00}
\acmISBN{978-1-4503-XXXX-X/18/06}

\input{defs}


\begin{document}

\title{Mechanized Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory}
\author{Eric Giovannini}
\affiliation{
  \department{Electrical Engineering and Computer Science}
  \institution{University of Michigan}
  \country{USA}
}
\email{ericgio@umich.edu}

\author{Max S. New}
\affiliation{
  \department{Electrical Engineering and Computer Science}
  \institution{University of Michigan}
  \country{USA}
}
\email{maxsnew@umich.edu}

\begin{abstract}
  Gradually typed programming languages, which allow for soundly
  mixing static and dynamically typed programming styles, present a
  strong challenge for metatheorists. Even the simplest sound
  gradually typed languages feature at least recursion and errors,
  with realistic languages featuring furthermore runtime allocation of
  memory locations and dynamic type tags. Further, the desired
  metatheoretic properties of gradually typed languages have become
  increasingly sophisticated: validity of typed based equational
  reasoning as well as the relational property known as the gradual
  guarantee or graduality. Many recent works have tackled verifying
  these properties, but the resulting mathematical developments are
  highly repetitive and tedious, with few reusable theorems persisting
  across different developments.

  In this work, we present a new denotational account of gradual
  typing semantics developed using guarded domain theory. Guarded
  domain theory combines the expressive power of step-indexed logical
  relations for modeling recursive features with the modularity and
  reusability of denotational semantics. Further, recent extensions to
  cubical Agda mean that synthetic guarded domain theory is readily
  mechanized in a proof assistant. We demonstrate the feasibility of
  this approach with a model of gradually typed lambda calculus and
  prove the validity of beta-eta equality and the graduality theorem
  for the denotational model. This model should provide the basis for
  a reusable mathematical theory of gradually typed program semantics.
%%     We develop a denotational semantics for a simple gradually typed language
%%     that is adequate and proves the graduality theorem.
%%     %
%%     The denotational semantics is constructed using \emph{synthetic
%%     guarded domain theory} working in a type theory with a later
%%     modality and clock quantification.
%%     %
%%     This provides a remarkably simple presentation of the semantics,
%%     where gradual types are interpreted as ordinary types in our ambient
%%     type theory equipped with an ordinary preorder structure to model
%%     the error ordering.
%%     %
%%     This avoids the complexities of classical domain-theoretic models
%%     (New and Licata) or logical relations models using explicit
%%     step-indexing (New and Ahmed).
%%     %
%%     In particular, we avoid a major technical complexity of New and
%%     Ahmed that requires two logical relations to prove the graduality
%%     theorem.
  
%%     By working synthetically we can treat the domains in which gradual
%%     types are interpreted as if they were ordinary sets. This allows us
%%     to give a ``na\"ive'' presentation of gradual typing where each
%%     gradual type is modeled as a well-behaved subset of the universal
%%     domain used to model the dynamic type, and type precision is modeled
%%     as simply a subset relation.
%%     %
  \end{abstract}

\maketitle

% Outline

% 1. Intro: What do we want out of gradually typed languages and why
%    is it hard to prove? Explanation: Gradual Typing inherently
%    involves recursive types, multiple effects, relational properties.
%    We argue that the increasing complexity of the metatheory of
%    gradual typing makes it a good candidate for 

% 2. Extensional Dream Semantics: double categorical

% 3. The Problem with Step-indexing

% 4. A Compromise

% 5. Formalization in Guarded Cubical Agda

\newif\ifdraft
\drafttrue
\renewcommand{\max}[1]{\ifdraft{\color{blue}[{\bf Max}: #1]}\fi}
\newcommand{\eric}[1]{\ifdraft{\color{orange}[{\bf Steven}: #1]}\fi}
\newcommand{\tingting}[1]{\ifdraft{\color{red}[{\bf Pedro}: #1]}\fi}

\input{intro}

\input{technical-background}

% \input{syntax}

% \input{semantics}

\input{terms}

\input{ordering}

\input{graduality}

\input{categorical-model}

%\input{denotational-model}
\input{concrete-model}

\input{discussion}


\bibliographystyle{ACM-Reference-Format}
\bibliography{references}

\appendix
\input{appendix}


% \section{Discussion}\label{sec:discussion}

% \subsection{Synthetic Ordering}

% While the use of synthetic guarded domain theory allows us to very
% conveniently work with non-well-founded recursive constructions while
% abstracting away the precise details of step-indexing, we do work with
% the error ordering in a mostly analytic fashion in that gradual types
% are interpreted as sets equipped with an ordering relation, and all
% terms must be proven to be monotone.
% %
% It is possible that a combination of synthetic guarded domain theory
% with \emph{directed} type theory would allow for an a synthetic
% treatment of the error ordering as well.


\end{document}