\documentclass[acmsmall,screen]{acmart}
\usepackage{mathpartir}
\usepackage{tikz-cd}
\usepackage{enumitem}
\usepackage{wrapfig}
\usepackage{fancyvrb}
\usepackage{comment}

\usepackage{ stmaryrd }


%% 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{Denotational Semantics for Gradual Typing in Synthetic Guarded Domain Theory}
\author{Eric Giovannini}
\author{Max S. New}


\begin{abstract}
    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

\input{intro}

\input{technical-background}

\input{syntax}

\input{semantics}

\input{graduality}

\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.


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

\end{document}