Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
\documentclass[acmsmall,screen]{acmart}
\usepackage{mathpartir}
\usepackage{tikz-cd}
%% 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}
\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 gradually typed language
with effects 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 require 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.
%
This provides a rich semantic setting in which to
\end{abstract}
\section{Introduction}
% gradual typing, graduality
% synthetic guarded domain theory, denotational semantics therein
% Difficulties in prior semantics
\section{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}