arXiv:1608.06012v1 [cs.PL] 21 Aug 2016

A Vision for Online Verification-Validation
Matthew A. Hammer

Bor-Yuh Evan Chang

David Van Horn

University of Colorado Boulder
matthew.hammer@colorado.edu

University of Colorado Boulder
evan.chang@colorado.edu

University of Maryland, College Park
dvanhorn@cs.umd.edu

Abstract

1
2

Today’s programmers face a false choice between creating software that is extensible and software that is correct. Specifically, dynamic languages permit software that
is richly extensible (via dynamic code loading, dynamic object extension, and various forms of reflection), and today’s
programmers exploit this flexibility to “bring their own language features” to enrich extensible languages (e.g., by using common JavaScript libraries). Meanwhile, such librarybased language extensions generally lack enforcement of
their abstractions, leading to programming errors that are
complex to avoid and predict.
To offer verification for this extensible world, we propose
online verification-validation (OVV), which consists of language and VM design that enables a “phaseless” approach to
program analysis, in contrast to the standard static-dynamic
phase distinction. Phaseless analysis freely interposes abstract interpretation with concrete execution, allowing analyses to use dynamic (concrete) information to prove universal
(abstract) properties about future execution.
In this paper, we present a conceptual overview of OVV
through a motivating example program that uses a hypothetical database library. We present a generic semantics for
OVV, and an extension to this semantics that offers a simple
gradual type system for the database library primitives. The
result of instantiating this gradual type system in an OVV
setting is a checker that can progressively type successive
continuations of the program until a continuation is fully
verified. To evaluate the proposed vision of OVV for this example, we implement the VM semantics (in Rust), and show
that this design permits progressive typing in this manner.

1.

let authors
let authorsUS

= openDb("authors.csv")
= filterDb(authors, (author) =>
author.citizenship === "US")

(a) Open a database with an implicit schema and filter the content.
name, citizenship, institution
Evan Chang, US, University of Colorado
Roly Perera, UK, University of Glasgow
Matthew Hammer, US, University of Colorado
David Van Horn, US, University of Maryland
(b) File authors.csv, example content.

Figure 1. Programming with dynamically-determined tables and objects in JavaScript

of field value—see Figure 1b for example content. In line 1
of Figure 1a, the programmer filters the author list down
to those that have US citizenship using the field projection
author.citizenship.
Suppose the programmer merely wants to know that
their code will not access undefined fields—-that, in this
respect, the program is well-typed. Given that these object fields are defined by the dynamic-generation of data
structures via openDb, the validity of this field projection
author.citizenship is generally unknowable until after line 1
when the structure of the authors table is defined based on
the contents of authors.csv. At the same time, this field projection is clearly valid because of the special first line in
specifically this authors.csv shown in Figure 1b.
There is a tension here between static and dynamic checking. On one hand, once the authors table has been determined, the programmer would like the field projections from
the rows to be statically verified. But on other hand, how
would static checking be feasible if the schema of authors
database is dynamically-determined—what would be the
type of the openDb function?
To resolve this tension, our key insight is to imagine
pausing the concrete execution of Figure 1a right after line 1
and before line 2. Then, imagine reflecting the continuation
of the program’s execution to apply abstract interpretation or
other static techniques to prove the validity of all subsequent
field projections on the rows of the authors table.
Our vision centers around a new paradigm for verification and validation that we call online verification-validation

Introduction

We consider the problem of typing unknown, dynamicallydetermined data obtained from the environment. To illustrate
what we mean by unknown, dynamically-determined data,
consider the code in Figure 1a that loads a comma-separated
value (CSV) file authors.csv using the openDb("authors.csv")
call on line 1. The contents of this file are organized into
lines, where each line is a row of field values. The first line
of the file is special and contains a list of field names instead

1

2016/8/23

(OVV). In contrast to today’s phasic analysis techniques,
OVV is phaseless: “static” analysis is freely interposed
with “dynamic” execution. By virtue of this mixed approach, OVV transcends the conventional phase distinctions
of “static” and “dynamic” analysis. To avoid confusion in
this phaseless setting, we refer to static analysis techniques
as those for ∀-analysis, since they demonstrate universal
properties of future program’s states. Likewise, we refer
to the techniques used in dynamic analysis as those for ∃analysis, since they demonstrate existential properties about
the past program’s states.
In this paper, we make the following contributions:

1
2
3
4

let authors
let authorsUS

= openDb("authors.csv")
= filterDb(authors, (author) =>
author.citizenship === "US")
let books
= openDb("books.csv")
let authbooksUS = joinDb(authorsUS, "name",
books, "author")
(a) The joinDb(db1,key1,db2,key2) library function accesses the key
fields using run-time reflection (e.g., db1[i][key1]).
author, title, year, publisher
...
(b) File books.csv, example content.

Figure 2. Continuing the example from Figure 1a with subsequent dynamically-determined data.

• We define λ-VMF, an abstract machine semantics that

enables a form of phaseless, online verification-validation
(Section 3). The key idea is annotating potentially faulting operations (e.g., field projection) with a certain (!) or
uncertain (?) flag, indicating whether or not that operation can be verified. Executing uncertain operations gets
stuck, so it is up to the OVV program to progressively
rewrite uncertain operations into certain ones by proving
the safety of the potentially faulting operation.

State
State Set

Dynamic / Concrete

Initial state

• We present a case study of instantiating online verifica-

tion-validation with a simple, bidirectional gradual type
system for dynamic field projection and databases with
dynamic schemas (Section 4). The result of instantiating
a gradual type system in an online verification-validation
setting is a checker that can progressively type successive
continuations of the program until a continuation is fully
verified (i.e., “statically” typed).

Line 1
Line 2

2
3
4
1
e
e
ne ine
in Lin
Li
L
Static Phase L
Initial
States

Line 3
Dynamic Phase

Line 4

(a) Phaseless, online verificationvalidation.

Initial
State

(b) Phasic, offline verification and
online validation.

Figure 3. Typical type checkers are phasic with an offline
static verifier and an online dynamic validator.
steps that compute over previously-defined data types (the
filtering and joining steps in lines 2 and 4).

• We implement the proposed design for λ-VMF in Rust

Phaseless Analysis. The essence of online verificationvalidation is pausing concrete execution to interleave it with
abstract interpretation. Pictorially, this interleaving of concrete and abstract execution can be visualized as a twodimensional grid, as in Figure 3a. The vertical axis represents the extent of concrete execution and dynamic, ∃analysis (measured by program line), and for each such
point, the horizontal axis represents the extent of abstract interpretation and static, ∀-analysis performed at this dynamic
execution point. As shown, abstract interpretation explores
the states after lines 2–4 after pausing at line 1, but revisits
the state after line 4 again after pausing at line 3. That is, we
imagine suspending the concrete execution of the program in
Figure 2a after the openDb call on line 1 and then interpreting
the continuation to statically compute, under an abstraction,
the set of reachable future states from this suspended current
state (the horizontal axis).
This online look-ahead would permit us to check the
projections of author.citizenship and db1[i]["name"] (on
lines 2 and 4, respectively) before the running program executes them concretely. However, the other projection in the
joinDb call on line 4—the projection of the author field (i.e.,
db2[j]["author"])—cannot be proven valid in this continua-

to demonstrate that the proposed instantiation of OVV
indeed realizes progressive typing. Our implementation
is public: https://github.com/cuplv/vmfuture.
In the next section, we dig deeper into what we term
online verification-validation by following the progressive
typing of the example program from Figure 1a.

2.

Static / Abstract
2
3
4
1
ne
ne ine
Li
Li
L
Li

ne

Overview

In Figure 2a, consider an extension of the example from
Figure 1a with two additional lines. The file books.csv is
opened on line 3 and contains a CSV file with book information (shown in Figure 2b). The final line (line 4) creates a
table of books written by US authors, along with the information about those authors.
Observe that this code alternates between dynamically
determining the types of the rows and tables (by reading the
two files authors.csv and books.csv on lines 1 and 3) and
computing over those tables (on lines 2 and 4). This example is a simple version of a pervasive pattern in dynamic languages, where execution interleaves dynamic steps that create new data types (the tables loaded in lines 1 and 3) and
2

2016/8/23

tion because the books.csv database has not yet been loaded.
But imagine similarly suspending the concrete execution
again after line 3 (shown as the bottom horizontal execution
in Figure 3a). Now in this continuation, an abstract interpretation can easily verify this last remaining projection on all
future concrete executions from this point.
For exposition, this example is short, and the distance between the concrete points for static checks and the future
concrete points of potential failure (a bad projection) are
tiny: they only consist of one or two lines. In the general
case, however, the distance between these points can be arbitrarily large. For instance, a long-running scientific workload may last days or weeks, and in these cases, it is critical
to know about possible future execution failures as soon as
possible, to minimize interruption due to programming errors.

1
2
3
4

function openDb(file) {
var table = openDbInternal(file)
{{ reflect/cc (chk_state, return table) }}
}

Figure 4. The openDb library function synthesizes a type for
the loaded table before returning via reflect/cc.

Online Verification-Validation. OVV programs consist of
two stratified layers that interact during execution. First, the
object layer expresses ordinary execution. Execution can escape into the meta layer, which is capable of inspecting the
run-time representation of the object layer. Code at the meta
layer expresses ∀-analysis and ∃-analysis over object programs. During ordinary execution, the meta layer plays a
passive role until special primitives transfer control. In particular, reflect/cc transfers control, along with a reflected
view of the current (object layer) continuation. Further, the
meta layer has access to read and write hidden annotations
on object layer values (e.g., to store program facts, such as
types). Collectively, these hidden annotations can be viewed
as providing a “shadow heap” for tracking dynamic, metalevel information, in the service of performing ∃-analyses.
For maximum extensibility, the object layer lacks a static
type system, relying on checking at the other layer. For convenience in expressing analysis over object programs, the
meta layer may employ a language that employs a static type
system (a la ML), but this is not a requirement. For concreteness in presentation, we use JavaScript syntax for object layer code and Rust-like syntax for meta layer code, and
we may consider language choice as an orthogonal concern.

Related Work: Traditional Analyses are Phasic. Typical,
existing program analyses impose phase distinctions between static and dynamic steps, forcing each phase to use
one approach or the other. At one extreme, today’s techniques for static verification explore all possible execution
paths, but have no knowledge of the dynamic execution environment. At the other extreme, dynamic validation explores
one path of execution: the path determined by concrete execution.
Type system design is, in general, a tradeoff in checking
in an offline, static phase (e.g., are function application expressions well-typed?) and checking in the online, dynamic
phase (e.g., is an array-index in bounds?). We illustrate this
phasic architecture in Figure 3b where the static and dynamic phases are sequenced and independent.
Some techniques attempt to “blend” these static and dynamic phases, so that information gleaned from one phase
feeds into the other. For instance, gradual typing [35, 36] enables shifting type checking between the static and dynamic
phases. Or, the notion of using a set of dynamic runs to glean
information before static verification appears several times
in the literature for call resolution [15], reflection instantiation [9] and for eval [20, 40]. We consider such techniques
phasic if there is some sequencing (rather than interleaving)
of static, ∀-analysis and dynamic, ∃-analysis phases.
While phasic analyses dominate the literature, there exist
some non-phasic analysis techniques, such as the “proofsfrom-tests” approach [6], that mix ∃-analysis information
during ∀-analysis (e.g., via directed-random automated testing [22]). In these works, the goal is to perform offline static
verification whose abstraction selection leverages ∃-analysis
information from testing. This is distinct from our vision,
where concrete execution is interposed with analyses (not
vice versa). However, this work shares our concern with incremental exploration of a state space, and it possible that
our proposed incremental substrate would also be beneficial
in the context of “proofs-from-tests.”

reflect/cc. The implementor of openDb uses reflect/cc to
mediate between concrete execution in the object layer,
and interposed code in the meta layer that performs online ∀-analysis (shown in Figure 4). First, openDb uses
openDbInternal to load the given file and construct a table
from its CSV content (line 2). Next, line 3 uses reflect/cc
to invoke the meta-level function chk_state, which determines types for the table’s content (failing with an error
if this content is malformed). As a side effect, it writes to a
meta layer field on the table variable to record the type of the
rows of the table so that it can be consumed in a subsequent
meta layer execution. In particular, the reflect/cc primitive
pauses the execution of the object program, giving control
to a meta language function, here chk_state. Before transferring control, the primitive reflects the current continuation as
a first-class data structure and uses it as an argument to the
given meta language code, here chk_state, as we illustrate in
Figure 5.
By using this reflected structure, the meta language code
can perform arbitrarily complex ∀-analysis. When it finishes,
it returns control to the object program by returning a transformed program state. In this case, openDb uses chk_stk to
type-check the program’s continuation at each call, given

3

2016/8/23

State
State Set

Object Language

reflect/cc

(either ∀-analysis or ∃-analysis). In particular, meta layer
function chk_stk performs a ∀-analysis (type-inference and
checking), and uses these universal program facts to improve
the efficiency of ∃-analyses that will occur in the future.
At a high level, chk_stk traverses the frames of a VM
stack (from top to bottom), and checks whether the form of
the frame is consistent with the given computation type ct.
There are three cases to consider, depending on whether the
stack is empty (Halt), or has a top-most frame for a let
binding or function application.
The computation type Ret(vt) indicates that the local continuation will return a value of type vt, and that the stack
should contain a let body that is expecting to bind this value.
The frame FrLet(env,x,e) consists of a saved VM environment env (mapping local variables to values), a variable to
let-bind x, and a body e in which the variable is scoped. To
check this case, the code first attempts to synthesize a typing environment from env; if this fails, the stack does not
check, and verification fails. Otherwise, the meta-level function syn_tenv synthesizes a typing environment and returns
an annotated version of the given environment, env2. Next,
the case attempts to synthesize a type et for the let body, e.
When successful, synthesis produces a type et and an annotated term e. Finally, the case checks the recursive structure
of the stack; when successful, it returns a transformed stack,
whose environments, terms and values are annotated.
The computation type Arr(vt,ct2) indicates that the local continuation is a function abstraction that will consume
a value of type vt, and that the stack should contain an argument value with this type. Similar to above, the case checks
the value has the correct type vt, and checks the stack recursively; when successful, it returns a transformed (annotated)
stack.

Meta Language
2
3
4
1
e
ne
ne ine
n
Li
Li
L
Li

Line 1
Line 2

1
2
3
4

Line 3
Line 4

(a) The transfer of control moves
from the object program to the meta
program via reflect/cc.

let
let
let
let

...
...
...
...

=
=
=
=

openDb(. . .)
filterDb(. . .)
openDb(. . .)
joinDb(. . .)

(b) Sketch of the example code
from Figure 2a.

Figure 5. Illustrating online verification-validation.

enum Stk {
Halt,
FrLet(Env,Var,Exp,Stk),
FrApp(Val,Stk)
}

enum CTyp {
Ret(VTyp),
Arr(VTyp, CTyp)
}

meta chk_stk (st:StTyp, stk:Stk, ct:CTyp) -> Option<Stk>
{ match (ct, stk) {
_,
Halt => Some(stk),
Ret(vt), FrLet(env, x, e, stk2) =>
{ match syn_tenv(st, env) { None => None,
Some(tenv,env2) =>
{ let tenv = tenv_ext(tenv, x, vt) ;
match syn_exp(st, tenv, e) { None => None,
Some(et, e2) =>
{ match chk_stack (st, stk2, et) { None => None,
Some(stk3) => Some(FrLet(env2, x, e2, stk3))
}}
}}
}}
Arr(vt,ct), FrApp(v,stk2) => {
match ( check_value(st, emp, v, vt),
check_stack(st, stk2, c) ) {
(Some(v3), Some(stk3)) => Some(App(v3,stk3)),
_
=> None,
}}
}}

Defining and using OVV. Below, Section 3 defines the
syntax and dynamic semantics of λ-VMF in detail; building
on these definitions, Section 4 revisits the algorithm shown
in Figure 6, showing it in the context of a larger system for
gradually-typing programs that compute with databases, like
the one shown in Figure 5.

Figure 6. Type checking continuations.
the type of the loaded table. Based on this type information,
openDb either signals errors (if there is a type error), or transforms future validation checks (if type analysis succeeds in
proving that these validation checks are redundant).

3.

OVV Machine Semantics

We present λ-VMF, an abstract machine semantics for
libraries and programs that employ OVV. In Section 4, we
instantiate this OVV framework with a gradual type system
for checking programs that compute with simple databases.

The Meta Program Expresses Online Meta Theory. Figure 6 lists the meta-layer function chk_stk, which checks a
VM stack against a store typing and computation type. We
adopt Rust-like syntax (a recent dialect of ML). In particular,
this meta-level code interacts with the store typing, stack and
computation types as values, as if they are persistent (purely
functional, applicative) inductively-defined structures, a la
ordinary ML. (The top of Figure 6 defines these structures
in Rust-like syntax). Because the meta layer has meta-level
access to the semantic structures of the object layer, it is
sufficiently powerful to compute meta-theoretical properties

Program Syntax. Figure 7 gives the syntax for λ-VMF
programs. To streamline the definition of analyses and dynamic interpretation, λ-VMF syntactically separates program structure into expressions e and values v . Further, to
permit a meta-layer, extension-defined analysis to annotate
λ-VMF programs (as illustrated in Section 4), the recursive
syntax of expressions and values consists of annotated preexpressions ė and annotated pre-values v̇, respectively. The
4

2016/8/23

operational semantics of λ-VMF programs, defined below,
does not directly depend on these annotations. However, an
extension may use its annotations to prove properties that
verify sound online program transformations. In these cases,
the annotations can indirectly impact program behavior, i.e.,
by aiding a meta-level program transformation.
Pre-values consist of open and closed thunks, which represent suspended expressions, including all higher-order
data (othunk e and thunk ρ e); closed thunks employ a
closing environment ρ that maps the free variables of e to
(closed) values. Base types consist of numbers (num n),
strings (str s), boolean bits (bool b) and reference cells (loc `).
Dictionaries map values to values (dict δ), modeling a row
of a database, or a record, where the typical notion of a field
name is generalized to any value in λ-VMF.
Pre-expressions consist of forcing a suspended expression (force v ), function abstraction (λx.e), function application (e v ), let-binding a returned value (let x = e1 in e2 ),
returning a value (ret v ), allocating, mutating and accessing mutable storage (ref v , set v1 v2 , get v , respectively),
updating the field of a record (ext v1 v2 v3 ), projecting the
field of a record (v1 [v2 ]aop ).
Finally, λ-VMF includes special forms for ascribing a
sub-expression with a manual annotation (e ?: ae ), and reflectively inspecting (and transforming) the current continuation via reflect/cc as core primitive, rcc em e. Notably,
execution pauses before executing the local continuation e,
and a common idiom consists of using a manual ascription
there, to be discharged via the use of rcc.
As explained below, using rcc to prove and discharge ascriptions is actually necessary in λ-VMF, since they have
no other form of dynamic semantics. For this purpose,
the meta-level program em transforms the program state before its continuation resumes. We do not model the modellevel programming language here; our current implementation uses Rust.
VM State syntax. Figure 8 defines the global state of the
λ-VMF program: It consists of a store, mapping locations to
mutable values (µ); a stack of evaluation context frames (κ),
an environment mapping variables to values (ρ), and a preexpression ė that gives the current local continuation. Nonempty stacks give evaluation contexts for let bodies (κ ::
(ρ, x.e)) and function application (κ :: v ).

v ::= v̇ @: av
v̇ ::= othunk e
| thunk ρ e
| dict δ
| num n
| str s
| bool b
| loc `
| ()
|x
δ ::= ε | δ, v1 7→ v2

Value
Pre-Val.

Dict.

e ::= ė @: ae
ė ::= force v
| λx.e
|ev
| let x = e1 in e2
| ret v
| ref v
| set v1 v2
| get v
| ext v1 v2 v3
| v1 [v2 ]aop
| e ?: ae
| rcc em e
aop ::= ? | !
av ::= · · ·
ae ::= · · ·
em ::= · · ·

Expr.
Pre-Expr.

Annot.

Meta Expr.

Annotated pre-value
Open thunk
Closed thunk
Dictionary
Number
String
Boolean
Store location
Unit value
Value variable
Dictionaries of values
Annotated pre-expression
Unsuspend (force) thunk
Function abstraction
Function application
Bind computed value
Produce a value
Allocate store reference
Store mutation
Store projection
Dictionary extension
Dictionary projection
Annotation ascription
Reflect current continuation
Uncertain vs. certain
Value annotation
Expression annotation
Meta-level programs

Figure 7. Syntax of λ-VMF Programs
State
Store
Stack

Environment

σ ::= hµ; κ; ρ; ėi
µ ::= ε | µ, ` 7→ v
κ ::= halt
| κ :: (ρ, x.e)
| κ :: v
ρ ::= ε | ρ, x 7→ v

Maps locations to values
Empty stack
Waiting for return
Fun. application argument
Maps variables to values

Figure 8. VM State: The store, stack and environment.
a (possibly empty) dictionary; and dictionary projection selects a given field’s associated value, returning it.
What makes λ-VMF particularly interesting is that there
are no stepping rules for ?-mode field projection or for ascription. To avoid getting stuck at these operations, these operations should be either verified progressively or validated,
perhaps immediately before executing, when all relevant information is available. To do so, the program uses rcc em e,
which runs the meta-level program em on a reflected version of the current VM state: the rule constructs the current
continuation, reflects this program state into a data structure, runs the meta-level term em , and then injects the resulting program state into a transformed continuation σ 0 . In
OVV, this step sometimes verifies and validates operations
before the program attempts to execute them, transforming

Dynamics of λ-VMF Programs. Figure 9 defines a smallstep operational semantics over λ-VMF states. The rules for
let and function application each push the stack with a frame
that is eliminated by the rules for ret and function abstraction, respectively. In both cases, eliminating the frame consists of binding a value to a variable, and continuing the program. Forcing a thunk consists of unpacking its environment
and expression, and continuing execution with them. Rules
for allocating, mutating and accessing a reference cell in the
store are each standard. Dictionary extension adds a field to
5

2016/8/23

σ −→ σ 0 λ-VMF state σ steps to state σ0 .
hµ; κ; ρ
hµ; κ; ρ
hµ; κ :: (ρ, x.(ė @: )); ρ0
hµ; κ :: v ; ρ
hµ; κ; ρ
hµ; κ; ρ
hµ; κ; ρ
hµ, ` 7→ v2 ; κ; ρ
hµ; κ; ρ
hµ; κ; ρ

let x = (ė1 @: ) in e2 i
(ė @: ) v i
ret v i
λx.(ė @: )i
force v i
ref v i
set v1 v2 i
get v1 i
ext v1 v2 v3 i
v1 [v2 ]!

−→
−→
−→
−→
−→
−→
−→
−→
−→
−→

hµ; κ :: (ρ, x.e2 ); ρ; ė1 i
hµ; κ :: ρ(v ); ρ; ėi
hµ; κ; ρ, x 7→ ρ(v ); ėi
hµ; κ; ρ, x 7→ v ; ėi
hµ; κ; ρ0 ; ėi
hµ, ` 7→ v ; κ; ρ; ret (loc ` @: ?)i
hµ, ` 7→ ρ(v2 ); κ; ρ; ret (() @: ?)i
hµ, ` 7→ v2 ; κ; ρ; ret v2 i
hµ; κ; ρ; ret (dict (δ, ρ(v2 ) 7→ ρ(v3 )) @: ?)i
hµ; κ; ρ; ret v3 i

hµ; κ; ρ
hµ; κ; ρ

v1 [v2 ]?
e ?: ae i

no stepping rule
no stepping rule

hµ; κ; ρ

rcc em (ė @: )i

−→

σ0

when
when
when
when
when
when

ρ(v ) = (thunk ρ0 (ė @: ) @: )
` 6∈ µ
ρ(v1 ) = (loc ` @: )
ρ(v1 ) = (loc ` @: )
ρ(v1 ) = (dict δ @: )
ρ(v1 ) = (dict (δ, ρ(v2 ) 7→ v3 ) @: )

when

em ([[hµ; κ; ρ; ėi]]) ⇓meta [[σ 0 ]]

Figure 9. Small-step, abstract machine semantics of λ-VMF
e ::= · · ·
| openDbaop v
| filterDbaop v1 v2
| joinDbaop v1 v2 v3 v4

Existing forms (Figure 7)
Open database by file path
Filter DB by predicate
Join DBs using keys’ value

Annotations
Value Types

Figure 10. Database Library Forms

the program to remove or modify them. In contrast to traditional phasic static verification or dynamic validation (cf.
Figure 3b), this step does not need to be either eagerly before the entire execution or lazily just before the potentially
faulting operation. By choosing the placement of rcc, the
program can choose how eager or lazy the checking should
be anywhere between these two extremes. We give a detailed
example below.

4.

Dictionary
Computation
Types

av ::= A
ae ::= C
A, B ::= U C
| Dict ∆
| Num
| Str
| Bool
| Ref A
|1
|?
| Db A
∆ ::=

Value annotation
Expression annotation
Thunked computation
Dictionary
Number
String
Boolean
Reference cell
Unit
Unknown value type
Database; multiset of As

ε | ∆, v 7→ A Maps values to types

C , D ::= A → C
| FA

Function abstraction
Value production

Figure 11. Type Syntax: Annotations for Values and Expressions

Gradual Typing for Simple Databases
Types for λ-VMF and libDb. Figure 11 instantiates the
λ-VMF framework for a gradual type system. This system has (bidirectional, algorithmic) rules to reason about
λ-VMF code as well as the libDb extension. Value types
consist of types for thunked computations (U C ) 1 , dictionaries (Dict ∆, where ∆ maps field values to field types),
numbers (Num), strings (Str), booleans (Bool), reference cells (Ref A), unit (1), unknown (?) and databases
(Db A). Computation types consist of the arrow type for
functions (A → C ) and value types for value-producing
computations (F A).

In this section we present a gradual type system for λVMF and libDb, an extension that permits us to express the
motivating example from Figure 2a. We tour the type system
and illustrate how OVV progressively types and validates the
operations in this example.
Syntax for libDb. Figure 10 extends the syntax from Figure 7 with the three operations implemented by libDb, for
opening databases, filtering them with a predicate, and joining them using named fields. Each operation is parameterized by one or more argument values, and an operation annotation aop that determines how to type operation. As with
record field projection, this annotation determines whether
the operation’s pre-conditions for success have been fully
verified via OVV. The gradual type system for libDb presented here uses different rules for certain (!) versus uncertain (?) reasoning modes.

Typing λ-VMF program states. Figure 12 lists typing
judgement forms for λ-VMF program states and for stacks.
1

We follow conventions from the literature on call-by-push-value (CBPV)
in our type syntax for thunked and value-returning computations, which
uses special letters U and F, respectively [29, 30].

6

2016/8/23

hold, in the case of true, we also construct an annotated
term, possibly with transformations (e.g., changing operation annotations from uncertain ? to certain !).
|µ| ` ρ ⇒ Γ
|µ| , Γ ` ė ⇒ C
|µ| ` κ ⇐ C
state
For instance, we implement the type relation for program
hµ; κ; ρ; ėi ok
states as a total function from program states to (optional)
Γ ` κ ⇐ C Under Γ, stack κ eliminates a computation of type C . program states with annotations; and when the algorithm
fails, it returns None: Furthermore, this algorithm plays the
role of em in libDb’s use of rcc em e.
Γ1 ` ρ ⇒ Γ2
The ability to phrase the typing relations as functional alΓ2 , x : A ` e ⇒ C
Γ1 ` κ ⇐ C
gorithms stems the fact that the rules treat certain positions
k-emp
k-let
of their (bidirectional) relations consistently as inputs and
Γ ` halt ⇐ C
Γ1 ` κ :: (ρ, x.e) ⇐ F A
outputs, and that outputs are determined functionally from
Γ`v ⇐A
inputs. As an example, Figure 6 gives the algorithmic verΓ`κ⇐C
sion of the stack-checking relation Γ ` κ ⇐ C , which rek-app
Γ ` κ :: v ⇐ A → C
sembles an ordinary function in ML. The remainder of the
rules transform in a similar manner, so that checking relations produce an optional, annotated term structure, while
Figure 12. Stack typing and State typing
synthesizing relations produce an optional pair of annotated
term structure and synthesized type. When these functions
produce None, the corresponding typing relation is not derivTo type a program state, we assume that the stored values
able. The dynamic semantics of λ-VMF do not permit exeare annotated, and we use these annotations as a store typcution to continue when this occurs.
ing, written |µ|, which maps reference locations to values
types. To type a program state, we assume this store typTyping core λ-VMF terms bidirectionally. For simplicity,
ing |µ| and attempt to verify the the other VM machinery,
we use a bidirectional type system to encode the gradual type
consisting of the current environment ρ, program term ė,
systems of the λ-VMF core calculus and its libDb extension.
and stack κ. Three judgements compute type properties for
Figure 13 defines type checking (above) and synthesis (bethese components: Assuming a store typing Γ, the judgelow) for program terms. For space reasons, we elide some
0
ment Γ ` ρ ⇒ Γ computes from an environment (mapsynthesis cases, as well as the checking and synthesis judge0
ping variables to values), a typing context Γ (mapping variments for value forms; the rules shown give a representative
ables to types). Assuming a typing context Γ, the judgement
flavor for the complete definition.
Γ ` e ⇒ C computes a type from a term e. Assuming
The analytical (checking) judgement form Γ ` e ⇐ C
a typing context Γ and computation type C for a terminal
can
be read as, “Under typing context Γ, term e checks
computation, the judgement Γ ` κ ⇐ C checks that the
against
computation type C .” Specifically, the type C is
stack κ either correctly continues execution or halts.
given
as
an input to the checking judgement, when viewed as
The remainder of the figure gives three rules for typean
algorithm.
The synthesizing judgement form Γ ` e ⇒ C
checking the stack. First, k-emp says that halting stacks are
can
be
read
as,
“the typing context Γ and term e synthesize
always permitted. Next, k-let and k-app handle the recursive
the
computation
type C .” Specifically, the algorithm comcases of the stack, where the topmost frame can be viewed as
putes
the
type
C
,
when given Γ and e. For the core forms
eliminating the terminal computation type, call it D. In the
of
λ-VMF,
the
bidirectional
rules for values and computacase of k-let, we have that D is F A, which types the terminal
tions
follow
the
usual
patterns
found in bidirectional type
computation that returns a value of type A; we check that the
systems
[10,
16].
We
show
several
standard-looking rules,
top of the stack holds the body of the let, which can use the
sub,
lam,
app
and
annot.
In
particular,
the annotation form of
let-bound variable (of type A), for which we can synthesize
e
λ-VMF,
e
?:
a
,
which
asserts
the
annotation
ae correctly
another computation type C that checks against the rest of
describes the program e, plays the role of type ascription
the stack. In the case of k-app, we have that D is A → C ,
in the bidirectional rules; the annot rule says that terms are
the type of a function abstraction; we check that the top of
checked against their type annotations, and these annotated
the stack is an argument value of type A, and the rest of the
terms synthesize the annotation type. Because it has no dystack checks against the type of the abstraction’s body, C .
namic semantics, λ-VMF uses OVV to prove and discharge
Transforming λ-VMF program states. Though the gradthis form earlier by rewriting it to e sometime before evalual type system defined here is stated propositionally, it conuation; if this rewrite fails, then the program terminates (by
stitutes an algorithm, and we demonstrate this fact by implefailing) early, as a result of OVV failing, not execution.
menting these relational definitions as a (mutually) recursive
As is customary in bidirectional systems, type annotatotal functions. However, instead of merely returning true
tions mediate between synthesizing and checking. This proor false to indicate the success or failure of the relation to
vides one the ability to place checking-only terms (such as

σ ok State σ is well-typed.

7

2016/8/23

lambda abstractions) in positions that require the sub-term
synthesize a type (such as the abstraction position of an application). See typing rules lam and app, respectively, to see
the details; both are standard. Finally, as is customary, type
subsumption allows less specific types to check against terms
that synthesize more specific types. Rule sub uses a definition of type consistency (written C ≈? D), which behaves
like type equality, modulo the uncertain type ?, which is
consistent with all other types. This notion of consistency
is standard in some gradual typing literature [35].

Γ ` e ⇐ C Under Γ, expression e checks against type C .
Γ`e⇒C
C ≈? D
Γ`e⇐D

Γ, x : A ` e ⇐ C

sub

Γ ` λx.e ⇐ A → C

lam

Γ ` e ⇒ C Under Γ, expression e synthesizes type C .
Γ`e⇐C
Γ ` e ?: C ⇒ C
Γ ` v1 ⇒ ?
Γ ` v2 ⇒ B
Γ ` v1 [v2 ]? ⇒ F ?

Γ`e⇒A→C
Γ`v ⇐A

annot

p?

Γ`ev ⇒C

Γ ` v1 ⇒ Dict (∆, v2 7→ A)
Γ ` v2 ⇒ B
Γ ` v1 [v2 ]! ⇒ F A

Γ ` v ⇒ Str
Γ ` openDb? v ⇒ F (Db ?)

Gradual typing for dictionary projection. The typing rules
for uncertain and certain projection differ in what is known
about the record and field values, and illustrate a form of
gradual typing. In the uncertain case, rule p? synthesizes
return type ?, since nothing is known about the dictionary
of values being projected. By contrast, in the certain case,
the dictionary type is known to rule p!, and this dictionary
maps the given field value to a corresponding field type. In
this case, the soundness of the type system means that the
projection must succeed in all possible future program states,
and moreover, that the projected value has the given type.

p!

openDb?

Γ ` v1 ⇒ Db ?
Γ ` v2 ⇐ U (? → F Bool)
Γ ` filterDb? v1 v2 ⇒ F (Db ?)
Γ ` v1 ⇒ Db A
?∈
/A
Γ ` v2 ⇐ U (A → F Bool)
Γ ` filterDb! v1 v2 ⇒ F (Db A)
Γ ` v1 ⇒ Db ?
Γ ` v3 ⇒ Db ?

app

filterDb?

Typing the libDb operations. The rule openDb? is uncertain and has no certain counterpart: The type of the database
is not known until after the operation completes, just before execution resumes with its continuation; before then,
the database could hold any type, so the rule types the returned database as Db ?.
Following similar reasoning, since filtering and joining
databases occur after a database is loaded, it is possible to
type these operations in both uncertain and certain modes.
The rule filterDb? says that filtering a database of uncertain
values leads to another database of values with an uncertain
type; since it merely assumes the type of the database is ?,
it does not prove that the predicate will not “go wrong”,
e.g., by projecting the wrong field from its argument. By
contrast, the rule filterDb! says that filtering a database of
known type using a predicate that checks against this type
leads to a database with the same known type; in this case,
the soundness of the type system means that the predicate
must always succeed.
Similarly, the rules for joinDb? and joinDb! follow the
pattern set above: the uncertain rule assumes nothing about
the argument values, beyond the arguments actually consisting of databases. The certain rule assumes that the database
arguments’ types are fully known, that the chosen field values are mapped in these types, and that the chosen fields
share a common type (we want to compare values of this
field for equality to perform the join).

filterDb!

Γ ` v2 ⇒ B 2
Γ ` v4 ⇒ B 4

Γ ` joinDb? v1 v2 v3 v4 ⇒ F (Db ?)

joinDb?

∆ = ∆1 , v2 7→ A, ∆3 , v4 7→ A
Γ ` v1 ⇒ Db (Dict (∆1 , v2 7→ A))
Γ ` v2 ⇒ B2
Γ ` v3 ⇒ Db (Dict (∆3 , v4 7→ A))
Γ ` v4 ⇒ B4
Γ ` joinDb! v1 v2 v3 v4 : F (Db (Dict ∆))

joinDb!

Figure 13. Selected typing rules for computation typing
(checking and synthesis).

Typing (horizontal) across Execution (vertical).
Line 1
Line 2
Line 3
Line 4
openDb filterDb openDb joinDb
1: openDb
?
?
?
?
2: filterDb
—
!
?
?
3: openDb
—
—
?
?
4: joinDb
—
—
—
!

···
—
?
!/?
!/?
!

Figure 14. Progressive typing for Figure 2a: As execution
progresses (vertically) over Lines 1 and 3, the continuation’s
typing becomes more certain: After Line 1 executes, Line
2 types in the certain modality (!) instead of the uncertain
modality (?); similarly, after Line 3, Lines 4 onward type
using the certain modality. (The dashed horizontal lines indicate these progressions).

Gradual Typing, Progressively via OVV. Figure 14 illustrates using the typing rules of Figure 13 to perform progressive typing our four-line motivating example (Figure 2a).
The vertical and horizontal dimensions of the table list each
of the four lines; the vertical axis represents concrete ex8

2016/8/23

ecution, and the horizontal axis represents typing the four
right-hand-sides of the program’s four let-bindings, and in
particular, for filterDb (on Line 2) and joinDb (on Line 4),
the table indicates whether the operation was typed in the
uncertain or certain modality. As execution progresses (vertically) over Lines 1 and 3, the typing of the program continuation’s becomes more certain: After Line 1 executes, Line
2 types in the certain modality (!) instead of the uncertain
modality (?); similarly, after Line 3, Lines 4 onward type
using the certain modality. As the final column shows, the
certainty of code using these tables in the remainder of the
program (Line 5 onwards) increases after each of the two
calls to openDb. Between the two calls, some information is
known (relating to the first two tables defined on Lines 1 and
2), but some information is still missing (relating to the two
tables defined in Lines 3 and 4).
Our current Rust-based prototype of λ-VMF is powerful
enough to express this example, including the progressive
typing discussed above. In Section 5, we discuss the potential to use incremental computation in the context of such
progressive typing; the goal is to improve performance by
exploiting the redundancy of re-typing the program’s continuation.

5.

State
State Set

Concrete Execution

reflect/cc

State

Abstract Execution
2
3
4
1
ne ine
ne ine
L
Li
L
Li

reflect/cc

Abstract Execution
2
3
4
1
ne ine
ne ine
L
Li
L
Li

Validate
Residual

Line 1
Line 2

State Set

Progressive
Verification

δ

Line 3
Line 4

(a) Progressive verification

Regressive
Validation
Program
Transform

(b) Regressive validation

Figure 15. Progressive verification and regressive validation are complementary ways of seeing the interplay between ∀-analysis and ∃-analysis enabled by online
verification-validation.

be used to elide run-time ∃-analysis checks that concern
the authors table, including the asserts for the projections
of author.name. Pictorially, we think of regressive validation
as introducing a third dimension that consists of all possible outcomes of a program transformation on the object program (shown in Figure 15b). After performing an online verification, the meta layer transforms the continuation, either
eliding certain downstream validation checks (labeled validate), or introducing residual checks that reduce the original checks’ complexity (labeled residual). As illustrated in
Section 4, progressive typing can, before executing the operation, eliminate residual checks by rewriting uncertain operations to certain operations (which require no run-time type
checks). More aggressive verification techniques can hope
to regress even more aggressive validation checks to simpler
forms. For instance, global heap-based properties present an
interesting challenge.

Discussion

In this section, we discuss future challenges and directions for the vision of OVV presented in this paper. Specifically, we discuss the design of the meta-level programming
language, and its use in expressing progressive verification
and regressive validation.
Incremental Computation for Progressive Verification.
In the motivating example from Section 2, the chk_stk calls
performed by openDb use progressive typing to check their
continuations. In fact, these two continuations are related:
The earlier version lacks type information about the table
loaded in line 3, whereas the later version has access to this
type information. Progressive typing could exploit this incremental relationship to avoid re-computing all of the typing
facts about the program state that have not changed.
Progressive typing is a specific instance of progressive
verification. Pictorially, progressive verification relates distinct abstract executions (shown horizontally in Figure 15a),
by exploiting their similarity (a small change, depicted as δ,
extending vertically). The task of a progressive verifier is a
∀-analysis, just like a classical static verifier, which attempts
to prove that all executions to an assertion satisfy a particular
safety property.

Implicitly-Incremental Meta-Level Computation. In sum,
the example chk_stk above encodes a theory about online
typing, along with a mechanism for using this type information to optimize the dynamic run-time checks that would otherwise be used. The meta layer should have an in-built ability to implicitly express progressive verification as ordinary
verification, so that the system, not the programmer, takes
into account execution environment changes across these
progressive stages. Further, when the meta layer uses this
progressive verification to enable regressive validation in the
future execution down stream, the system, not the programmer, accounts for these changes when doing future stages of
progressive verification. In other words, the VM that runs the
meta language and object language should have an in-built
ability to express interaction among the levels in terms of
implicitly-incremental computation. In Section 6, we discuss
the challenges that OVV poses to work on general-purpose
incremental computation.

More Aggressive Regressive Validation. After type checking the continuation for line 1, regressive validation consists of eliminating dynamic checks within the library calls
of lines 2 and 4 (filterDb and joinDb, respectively). In particular, if the continuation type-checks under the partiallyknown type information, the known type information can
9

2016/8/23

6.

and implement reflective towers in simpler terms; these efforts are named after various hair colors: Brown [19, 39],
Blond [13] and most recently, Black [3, 4].
Compared to the impressive and mind-bending work on
metacircular interpreters, the vision for λ-VMF is more
modest: Two levels suffice to perform OVV. Having said
that, if meta-level programmers want to verify their metalevel programs as object programs (to “bootstrap” a typed
meta level), the work mentioned above will likely provide
further insights.

Related Work
This section supplements the related work in Section 2.

General-Purpose Incremental Computation. Section 5
proposes an implicitly incremental meta-level language for
λ-VMF, which challenges current research on (generalpurpose, programming language-based) incremental computation (IC). Consider the desired incremental behavior of
chk_stk in the motivating example, where it occurs after lines
1 and 3, when the program states are similar, but not identical. In particular, both continuations include the AST of
the call in line 4, and onward, which chk_stk will process
in both verification stages. The central challenge is reusing
the redundant work performed by chk_stk, despite the fact
that the AST and store typing are not equal to that in the
prior stage, which creates challenges for incremental computing via memoization, a key implementation mechanism
used across many specific IC approaches.
To understand why these “small” changes are challenging
for typical memoization, consider the structural recursion of
the chk_stk function from Figure 6. One approach to memoization identifies each saved invocation by the entire store
typing st and entire stack stk, including all of their recursive sub-structure, e.g., via hash-consing [18]. This approach
is commonly taken by past work on incremental computation [7, 8, 17, 23, 24, 32, 33, 33], however, it is brittle and
overly sensitive to small changes, since they alter the identity
of the whole recursive structure. Recent work addresses this
shortcoming by introducing unique names that are special
to incremental computing [25]. This naming mechanism can
overcome the challenges outlined above for chk_stk, since
the presence of names isolates changed components of the
store typing, stack and local environments.
However, several key challenges remain before these
techniques can fully realize OVV: We want to use these
names correctly (to avoid unsound incremental results), use
them efficiently (to isolate changes and avoid sub-redundant
computations) and use them implicitly (so that the meta-level
programs look like ML). Further, we may want to control
how fine-grained the IC techniques track program dependencies, to reduce constant-factor overhead.

Program Analysis for Dynamic Languages. The ultimate
aim of online verification-validation is offer “strong checking” in an extensible, dynamic language environment. And
thus we seek to build on the substantial amount of research
activity on program analysis for dynamic languages. Since
by definition, dynamic languages lack a built-in static typing
discipline, much of the static verification work focuses on
either retrofitting rich typing or specification disciplines [11,
12, 21] or applying whole-program flow analysis for inferring and checking type properties (e.g., for JavaScript [5, 26,
27] or for Ruby [1]).
The dynamic language features that make widely-used libraries like jQuery possible also make retrofitting static techniques incredibly challenging [2, 28, 34, 38]. Much of this
work focuses on finding the right kinds of context-sensitivity
to try to more precisely resolve the flow of values to dynamic features like dynamic property read in a static analysis [2, 31, 38] or to determine when dynamically-observed
information is sufficient to apply in a static verification [34].
We expect such techniques to be not only applicable and useful but strengthened in an OVV context. In the end, static
techniques in a phasic setting are limited by what is indeed
available statically, and dynamic techniques are limited by
what can be observed in testing runs. As exhibited in Section 2, the vision of OVV enables these techniques to be
strengthened with a flexible interleaving of “static” and “dynamic” analysis (i.e., ∀-analysis and ∃-analysis).

7.

Conclusion

This paper presents a vision for online verificationvalidation (OVV), an approach to ease the tension between
extensibility (of dynamic languages) and safety (of static
languages). The key insight of OVV is that analysis in a VM
can be phaseless, allowing analyses to run progressively on
the object program by pausing execution, reflecting on the
current continuation, and transforming the continuation to
replace uncertain (?) operations with certain (!) ones.
In this paper, we formalize an approach for OVV as a language semantics and Rust-based implementation called λVMF. We explore a proof-of-concept instantiation of OVV
by defining a gradual type system for dynamic field projection and databases with dynamic schemas, and we observed
that the result is a progressive type checker.

Reflective Towers of Interpreters. As proposed in Section 5, future work on λ-VMF should permit library extension authors to write meta programs and object programs in
an integrated way. Fortunately, many researchers have proposed designs that allow interesting interplay between the
interpreter’s viewpoint (where the meta-level program runs)
and the program being interpreted (where the object program
runs). Conceptually, this work begins with 3-LISP [14, 37],
which gives the programmer access to an infinite tower of
(so-called meta-circular) interpreters, allowing them to redefine the language from within the language. Following
(theoretical) work on 3-LISP, researchers give various approaches that attack practical concerns in how to express
10

2016/8/23

References

morphism with existentials and indexed types.
abs/1601.05106, 2016.

[1] Jong-hoon (David) An, Avik Chaudhuri, and Jeffrey S. Foster.
Static typing for Ruby on Rails. In Automated Software
Engineering (ASE), 2009.

[17] Sebastian Erdweg, Oliver Bracevac, Edlira Kuci, Matthias
Krebs, and Mira Mezini. A co-contextual formulation of
type rules and its application to incremental type checking.
In Object-Oriented Programming Systems, Languages, and
Applications (OOPSLA), 2015.

[2] Esben Andreasen and Anders Møller. Determinacy in static
analysis for jQuery. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2014.

[18] Jean-Christophe Filliâtre and Sylvain Conchon. Type-safe
modular hash-consing. In Proceedings of the 2006 Workshop
on ML. ACM, 2006.

[3] Kenichi Asai. Reflection in direct style. In Generative Programming and Component Engineering (GPCE), 2011.

[19] Daniel P. Friedman and Mitchell Wand. Reification: Reflection without metaphysics. In LISP and Functional Programming, 1984.

[4] Kenichi Asai, Satoshi Matsuoka, and Akinori Yonezawa. Duplication and partial evaluation for a better understanding of
reflective languages. Lisp and Symbolic Computation, 9(2-3),
1996.

[20] Michael Furr, Jong hoon (David) An, and Jeffrey S. Foster.
Profile-guided static typing for dynamic scripting languages.
In Object-Oriented Programming Systems, Languages, and
Applications (OOPSLA), 2009.

[5] SungGyeong Bae, Hyunghun Cho, Inho Lim, and Sukyoung
Ryu. SAFEWAPI: web API misuse detector for web applications. In Foundations of Software Engineering (FSE), 2014.

[21] Philippa Gardner, Sergio Maffeis, and Gareth David Smith.
Towards a program logic for JavaScript. In Principles of
Programming Languages (POPL), 2012.

[6] Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani,
Robert J. Simmons, Sai Deep Tetali, and Aditya V. Thakur.
Proofs from tests. IEEE Transactions on Software Engineering, 2010.

[22] Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART:
Directed automated random testing. In Programming Language Design and Implementation (PLDI), 2005.

[7] Pramod Bhatotia, Alexander Wieder, Rodrigo Rodrigues,
Umut A. Acar, and Rafael Pasquin. Incoop: MapReduce
for incremental computations. In Cloud Computing (SoCC),
2011.

[23] Philip J. Guo and Dawson Engler. Using automatic persistent
memoization to facilitate data analysis scripting. In Software
Testing and Analysis (ISSTA), 2011.

[8] Pramod Bhatotia, Pedro Fonseca, Umut A. Acar, Björn B.
Brandenburg, and Rodrigo Rodrigues. iThreads: A threading
library for parallel incremental computation. In Conference
on Architectural Support for Programming Languages and
Operating Systems (ASPLOS), 2015.

[24] Matthew A. Hammer, Yit Phang Khoo, Michael Hicks, and
Jeffrey S. Foster. Adapton: Composable, demand-driven incremental computation. In Programming Language Design
and Implementation (PLDI), 2014.
[25] Matthew A. Hammer, Joshua Dunfield, Kyle Headley,
Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, and
David Van Horn. Incremental computation with names. In
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2015.

[9] Eric Bodden, Andreas Sewe, Jan Sinschek, Hela Oueslati,
and Mira Mezini. Taming reflection: Aiding static analysis
in the presence of reflection and custom class loaders. In
International Conference on Software Engineering (ICSE),
2011.
[10] Adam Chlipala, Leaf Petersen, and Robert Harper.
bidirectional type checking. 2005.

CoRR,

[26] Simon Holm Jensen, Anders Møller, and Peter Thiemann.
Type analysis for JavaScript. In Static Analysis (SAS), 2009.

Strict

[27] Vineeth Kashyap, Kyle Dewey, Ethan A. Kuefner, John
Wagner, Kevin Gibbons, John Sarracino, Ben Wiedermann,
and Ben Hardekopf. JSAI: a static analysis platform for
JavaScript. In Foundations of Software Engineering (FSE),
2014.

[11] Ravi Chugh, David Herman, and Ranjit Jhala. Dependent
types for JavaScript. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2012.
[12] Ravi Chugh, Patrick Maxim Rondon, and Ranjit Jhala. Nested
refinements: a logic for duck typing. In Principles of Programming Languages (POPL), 2012.

[28] Benjamin S. Lerner, Liam Elberty, Jincheng Li, and Shriram Krishnamurthi. Combining form and function: Static
types for jQuery programs. In Object-Oriented Programming
(ECOOP), 2013.

[13] Olivier Danvy and Karoline Malmkjær. Intensions and extensions in a reflective tower. In LISP and Functional Programming, 1988.

[29] Paul Blain Levy. Call-by-push-value: A subsuming paradigm.
In Typed Lambda Calculi and Applications (TLCA), 1999.

[14] Jim des Rivières and Brian Cantwell Smith. The implementation of procedurally reflective languages. In LISP and Functional Programming, 1984.

[30] Paul Blain Levy. Call-by-push-value: A Functional/imperative Synthesis, volume 2. 2003.

[15] Bruno Dufour, Barbara G. Ryder, and Gary Sevitsky. Blended
analysis for performance understanding of framework-based
applications. In Software Testing and Analysis (ISSTA), 2007.

[31] Changhee Park and Sukyoung Ryu. Scalable and precise static
analysis of JavaScript applications via loop-sensitivity. In
Object-Oriented Programming (ECOOP), 2015.

[16] Joshua Dunfield and Neelakantan R. Krishnaswami. Sound
and complete bidirectional typechecking for higher-rank poly-

[32] William Pugh.
Incremental Computation via Function
Caching. PhD thesis, Cornell University, 1988.

11

2016/8/23

[37] Brian Cantwell Smith. Reflection and semantics in Lisp. In
Principles of Programming Languages (POPL), 1984.

[33] William Pugh and Tim Teitelbaum. Incremental computation via function caching. In Principles of Programming Languages (POPL), 1989.

[38] Manu Sridharan, Julian Dolby, Satish Chandra, Max Schäfer,
and Frank Tip. Correlation tracking for points-to analysis
of JavaScript. In Object-Oriented Programming (ECOOP),
2012.

[34] Max Schäfer, Manu Sridharan, Julian Dolby, and Frank Tip.
Dynamic determinacy analysis. In Programming Language
Design and Implementation (PLDI), 2013.

[39] Mitchell Wand and Daniel P. Friedman. The mystery of the
tower revealed: A nonreflective description of the reflective
tower. Lisp and Symbolic Computation, 1(1), 1988.

[35] Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming
Workshop, 2006.

[40] Shiyi Wei and Barbara G. Ryder. Practical blended taint
analysis for JavaScript. In Software Testing and Analysis
(ISSTA), 2013.

[36] Jeremy G. Siek and Walid Taha. Gradual typing for objects.
In Object-Oriented Programming (ECOOP), 2007.

12

2016/8/23

