/
hazelnut-dynamics-LIVE2017.tex
223 lines (184 loc) · 9.2 KB
/
hazelnut-dynamics-LIVE2017.tex
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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
\PassOptionsToPackage{svgnames,dvipsnames,svgnames}{xcolor}
%% For double-blind review submission
\documentclass[acmsmall]{acmart}\settopmatter{printfolios=true}
%% For single-blind review submission
%\documentclass[acmlarge,review]{acmart}\settopmatter{printfolios=true}
%% For final camera-ready submission
%\documentclass[acmlarge]{acmart}\settopmatter{}
%% Note: Authors migrating a paper from PACMPL format to traditional
%% SIGPLAN proceedings format should change 'acmlarge' to
%% 'sigplan,10pt'.
%% Some recommended packages.
\usepackage{booktabs} %% For formal tables:
%% http://ctan.org/pkg/booktabs
\usepackage{subcaption} %% For complex figures with subfigures/subcaptions
%% http://ctan.org/pkg/subcaption
%% Cyrus packages
\usepackage{microtype}
\usepackage{mdframed}
\usepackage{colortab}
\usepackage{mathpartir}
\usepackage{enumitem}
\usepackage{bbm}
\usepackage{stmaryrd}
\usepackage{wasysym}
\usepackage{mathtools}
\newcommand{\todo}[1]{{\color{red} #1}}
\usepackage{hyperref}
%% Joshua Dunfield macros
\def\OPTIONConf{1}%
\usepackage{joshuadunfield}
% \newtheorem{theorem}{Theorem}[chapter]
% \newtheorem{lemma}[theorem]{Lemma}
% \newtheorem{corollary}[theorem]{Corollary}
% \newtheorem{definition}[theorem]{Definition}
\newtheorem{assumption}[theorem]{Assumption}
\newtheorem{condition}[theorem]{Condition}
%% Listings
\makeatletter\if@ACM@journal\makeatother
%% Journal information (used by PACMPL format)
%% Supplied to authors by publisher for camera-ready submission
\acmJournal{PACMPL}
\acmVolume{1}
\acmNumber{1}
\acmArticle{1}
\acmYear{2017}
\acmMonth{1}
\acmDOI{10.1145/nnnnnnn.nnnnnnn}
\startPage{1}
\else\makeatother
%% Conference information (used by SIGPLAN proceedings format)
%% Supplied to authors by publisher for camera-ready submission
\acmConference[PL'17]{ACM SIGPLAN Conference on Programming Languages}{January 01--03, 2017}{New York, NY, USA}
\acmYear{2017}
\acmISBN{978-x-xxxx-xxxx-x/YY/MM}
\acmDOI{10.1145/nnnnnnn.nnnnnnn}
\startPage{1}
\fi
%% Copyright information
%% Supplied to authors (based on authors' rights management selection;
%% see authors.acm.org) by publisher for camera-ready submission
\setcopyright{none} %% For review submission
%\setcopyright{acmcopyright}
%\setcopyright{acmlicensed}
%\setcopyright{rightsretained}
%\copyrightyear{2017} %% If different from \acmYear
%% Bibliography style
\bibliographystyle{ACM-Reference-Format}
%% Citation style
%% Note: author/year citations are required for papers published as an
%% issue of PACMPL.
\citestyle{acmauthoryear} %% For author/year citations
\input{macros}
\begin{document}
%% Title information
\title{Toward a Live Stepper for Typed Expressions with Holes} %% [Short Title] is optional;
%% when present, will be used in
%% header instead of Full Title.
% \titlenote{with title note} %% \titlenote is optional;
%% can be repeated if necessary;
%% contents suppressed with 'anonymous'
% \subtitle{Subtitle} %% \subtitle is optional
% \subtitlenote{with subtitle note} %% \subtitlenote is optional;
%% can be repeated if necessary;
%% contents suppressed with 'anonymous'
%% Author information
%% Contents and number of authors suppressed with 'anonymous'.
%% Each author should be introduced by \author, followed by
%% \authornote (optional), \orcid (optional), \affiliation, and
%% \email.
%% An author may have multiple affiliations and/or emails; repeat the
%% appropriate command.
%% Many elements are not rendered, but should be provided for metadata
%% extraction tools.
%% Author with single affiliation.
\author{Cyrus Omar}
% \authornote{with author1 note} %% \authornote is optional;
%% can be repeated if necessary
% \orcid{nnnn-nnnn-nnnn-nnnn} %% \orcid is optional
\affiliation{
% \position{Position1}
% \department{Department1} %% \department is recommended
\institution{Carnegie Mellon University} %% \institution is required
% \streetaddress{Street1 Address1}
% \city{City1}
% \state{State1}
% \postcode{Post-Code1}
% \country{Country1}
}
\email{comar@cs.cmu.edu} %% \email is recommended
%% Author with two affiliations and emails.
\author{Ian Voysey}
% \authornote{with author2 note} %% \authornote is optional;
%% can be repeated if necessary
% \orcid{nnnn-nnnn-nnnn-nnnn} %% \orcid is optional
\affiliation{
% \position{Position2a}
% \department{Department2a} %% \department is recommended
\institution{Carnegie Mellon University} %% \institution is required
% \streetaddress{Street2a Address2a}
% \city{City2a}
% \state{State2a}
% \postcode{Post-Code2a}
% \country{Country2a}
}
\email{iev@cs.cmu.edu} %% \email is recommended
\author{Matthew A. Hammer}
\affiliation{
% \position{Position2b}
% \department{Department2b} %% \department is recommended
\institution{University of Colorado Boulder} %% \institution is required
% \streetaddress{Street3b Address2b}
% \city{City2b}
% \state{State2b}
% \postcode{Post-Code2b}
% \country{Country2b}
}
\email{matthew.hammer@colorado.edu} %% \email is recommended
%% Paper note
%% The \thanks command may be used to create a "paper note" ---
%% similar to a title note or an author note, but not explicitly
%% associated with a particular element. It will appear immediately
%% above the permission/copyright statement.
% \thanks{with paper note} %% \thanks is optional
%% can be repeated if necesary
%% contents suppressed with 'anonymous'
%% Abstract
%% Note: \begin{abstract}...\end{abstract} environment must come
%% before \maketitle command
\begin{abstract}
To understand the dynamic behavior of an expression, programmers can use a ``stepper'' to interactively simplify the expression according to the dynamic semantics of the programming language. The problem that motivates this work is that a standard dynamic semantics assigns meaning only to complete, well-typed expressions, but there are situations where a programmer might want to explore the dynamic behavior of an expression well before it is complete. This paper proposes the development of a dynamic semantics for \emph{incomplete expressions}, which we take to mean expressions with \emph{holes}. Holes indicate portions of the expression that have yet to be filled in, or, following our recent work \cite{popl-paper}, that have a local type inconsistency that has yet to be resolved. The result would be a program editor where the programmer has access to the stepper at all times, not just when the program is in a complete state, and where evaluation does not stop immediately at the hole, but rather proceeds as far as possible past the hole.
Even this would not be entirely satisfying when engaging in live programming, where editing and evaluation are interleaved, because na\"ively, the programmer would need to restart the stepper after each edit. To address this problem, this paper further proposes a mechanism that tracks the dynamic environment around each hole as well as its evaluation status. This allows for the specification of a \emph{live stepper}, i.e. a stepper where evaluation can continue where it left off even after holes are filled in, because the current state of the stepper can be ``patched'' to accurately reflect each edit that was made.
This paper reports early conceptual progress in these directions. Many details have yet to be considered. We hope to discuss both the human aspects and the formal aspects of the design with the workshop participants.% The paper discusses how prior work on gradual type theory and contextual modal type theory has informed our research so far.
\end{abstract}
%% 2012 ACM Computing Classification System (CSS) concepts
%% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
% \begin{CCSXML}
% <ccs2012>
% <concept>
% <concept_id>10011007.10011006.10011008</concept_id>
% <concept_desc>Software and its engineering~General programming languages</concept_desc>
% <concept_significance>500</concept_significance>
% </concept>
% <concept>
% <concept_id>10003456.10003457.10003521.10003525</concept_id>
% <concept_desc>Social and professional topics~History of programming languages</concept_desc>
% <concept_significance>300</concept_significance>
% </concept>
% </ccs2012>
% \end{CCSXML}
% \ccsdesc[500]{Software and its engineering~General programming languages}
% \ccsdesc[300]{Social and professional topics~History of programming languages}
%% End of generated code
%% Keywords
%% comma separated list
% \keywords{keyword1, keyword2, keyword3} %% \keywords is optional
%% \maketitle
%% Note: \maketitle command must come after title commands, author
%% commands, abstract environment, Computing Classification System
%% environment and commands, and keywords command.
\maketitle
\input{intro}
% \input{calculus}
\bibliography{all.short}
\end{document}