some writing

paper-new/paper.tex

@@ -32,42 +32,83 @@
 
 \begin{document}
 
-\title{Denotational Semantics for Gradual Typing in Synthetic Guarded Domain Theory}
+\title{Mechanized Denotational Semantics of Gradual Typing using 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.
+  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.
-    %
+%%     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
+\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
+
 
 \input{intro}
 
@@ -98,4 +139,4 @@
 \bibliographystyle{ACM-Reference-Format}
 \bibliography{references}
 
-\end{document}
\ No newline at end of file
+\end{document}

paper-new/semantics.tex

+\section{Denotational Semantics}
+
+First, we define a denotational semantics of types and terms of the
+cast calculus by giving a standard monadic denotational semantics in
+the cartesian closed category of preorders and monotone functions,
+extended to model the primitives of gradual typing: the dynamic type,
+errors and type casts. The most interesting part of this semantics is
+the construction of the monad and the dynamic type.
+
+
+
 \section{Domain-Theoretic Constructions}\label{sec:domain-theory}
 
 In this section, we discuss the fundamental objects of the model into which we will embed
@@ -193,4 +204,4 @@ the usual semantics in the category of sets.
 \subsubsection{Term Precision via the Step-Sensitive Error Ordering}
 % Homogeneous vs heterogeneous term precision
 
-% \subsection{Logical Relations Semantics}
\ No newline at end of file
+% \subsection{Logical Relations Semantics}

paper-new/technical-background.tex

@@ -29,6 +29,38 @@ behave the same except that $M$ may error more.
 
 % synthetic guarded domain theory, denotational semantics therein
 
+\subsection{Operational Reduction Proofs}
+
+\subsection{Classical Domain Models}
+
+New and Licata \cite{newlicata} developed an axiomatic account of the
+graduality relation on cast calculus terms and gave a denotational
+model of this calculus using classical domain theory based on
+$\omega$-CPOs. This semantics has scaled up to an analysis of a
+dependently typed gradual calculus in \cite{asdf}. This meets our
+criterion of being a reusable mathematical theory, as general semantic
+theorems about gradual domains can be developed independent of any
+particular syntax and then reused in many different denotational
+models. However, it is widely believed that such classical domain
+theoretic techniques cannot be extended to model higher-order store, a
+standard feature of realistic gradually typed languages such as Typed
+Racket. Thus if we want a reusable mathematical theory of gradual
+typing that can scale to realistic programming languages, we need to
+look elsewhere to so-called ``step-indexed'' techniques.
+
+A series of works \cite{newahmed,newlicataahmed,newjamnerahmed}
+developed step-indexed logical relations models of gradually typed
+languages based on operational semantics. Unlike, classical domain
+theory, such step-indexed techniques are capable of modeling
+higher-order store and runtime-extensible dynamic types
+\cite{amalsthesis,nonpmetricparamorsomething,newjamnerahmed}. However
+their proof developments are highly repetitive and technical, with
+each development formulating a logical relation from first-principles
+and proving many of the same tedious lemmas without reusable
+mathematical abstractions. Our goal in the current work is to extract
+these reusable mathematical principles from these tedious models to
+make formalization of realistic gradual languages tractible.
+
 \subsection{Difficulties in Prior Semantics}
   % Difficulties in prior semantics
 
@@ -283,4 +315,4 @@ Figure \ref{fig:topos-of-trees-fix}.
   \label{fig:topos-of-trees-fix}
 \end{figure}
 
-% TODO global elements?
\ No newline at end of file
+% TODO global elements?