| CS-2020-01 | ||||
|---|---|---|---|---|
| Title | Revisiting the SPLITS Model: Towards an Enhanced Implementation | |||
| Authors | Mark Y. Iwanchyshyn, Bradley W. Kimmel and Gladimir V. G. Baranoski | |||
| Abstract | The first-principles model known as SPLITS (SPectral LIght Transport model for Sand) was developed by the Natural Phenomenon Simulation Group (NPSG) at the University of Waterloo. This model has been employed in a wide range of investigations involving particulate materials. In this report, we present the refinements made to the model’s implementation and introduce its enhanced version. | |||
| Date | February 23, 2020 | |||
| Report | CS-2020-01 (PDF) | |||
| CS-2020-02 | ||||
| Title | An Engineering View of Regulating AI in Canada’s Financial Institutions | |||
| Authors | Derek Rayside, Emily Huang and Ayush Kapur | |||
| Abstract | An adaptation of NHTSA’s Proposed Voluntary Guidance for Autonomous Vehicles to the context of Canada’s financial institutions. | |||
| Date | February 28, 2020 | |||
| Report | CS-2020-02 (PDF) | |||
| CS-2020-03 | ||||
| Title | A Semantics for the Essence of React | |||
| Authors | Magnus Madsen, Ondřej Lhoták and Frank Tip | |||
| Abstract |
Traditionally,
web
applications
have
been
written
as
HTML
pages
with
embedded
JavaScript
code
that
implements
dynamic
and
interactive
features
by
manipulating
the
Document
Object
Model
(DOM)
through
a
low-level
browser
API.
However,
this
unprincipled
approach
leads
to
code
that
is
brittle,
difficult
to
understand,
non-modular,
and
does
not
facilitate
incremental
update
of
user-interfaces
in
response
to
state
changes. React is a popular framework for constructing web applications that aims to overcome these problems. React applications are written in a declarative and object-oriented style, and consist of components that are organized in a tree structure. Each component has a set of properties representing input parameters, a state consisting of values that may vary over time, and a render method that declaratively specifies the subcomponents of the component. React’s concept of reconciliation determines the impact of state changes and updates the user-interface incrementally by selective mounting and unmounting of subcomponents. At designated points, the React framework invokes lifecycle hooks that enable programmers to perform actions outside the framework such as acquiring and releasing resources needed by a component. These mechanisms exhibit considerable complexity, but, to our knowledge, no formal specification of React’s semantics exists. This paper presents a small-step operational semantics that captures the essence of React, as a first step towards a long-term goal of developing automatic tools for program understanding, automatic testing, and bug finding for React web applications. To demonstrate that key operations such as mounting, unmounting, and reconciliation terminate, we define the notion of a well-behaved component and prove that well-behavedness is preserved by these operations. | |||
| Date | June 2, 2020 | |||
| Report | CS-2020-03 (PDF) | |||
| CS-2020-04 | ||||
| Title | A Simpler Representation for R(4, 4) | |||
| Authors | Huijing Yao, Stephen Mann and Qinchuan Li | |||
| Abstract | We look at an alternate basis for R(4, 4), and see how this alternate basis affects the scalar coefficients both in geometric formulas and in affine transformations in this space. In particular, the original basis used in R(4, 4) introduced powers of 2 into these formulas; with the new basis, most of these formulas are simpler, and do not have these powers of 2. | |||
| Date | July 6, 2020 | |||
| Report | CS-2020-04 (PDF) | |||
| CS-2020-05 | ||||
| Title | Fixpoints for the Masses: Programming with First-class Datalog Constraints | |||
| Authors | Magnus Madsen and Ondřej Lhoták | |||
| Abstract |
Datalog
is
a
declarative
logic
programming
language
that
has
been
used
in
a
variety
of
applications,
including
big-data
analytics,
language
processing,
networking
and
distributed
systems,
and
program
analysis. In this paper, we propose first-class Datalog constraints as a mechanism to construct, compose, and solve Datalog programs at run time. The benefits are twofold: We gain the full power of a functional programming language to operate on Datalog constraints-as-values, while simultaneously we can use Datalog where it really shines: to declaratively express and solve fixpoint problems. We present an extension of the lambda calculus with first-class Datalog constraints, including its semantics and a type system with row polymorphism based on Hindley-Milner. We prove soundness of the type system and implement it as an extension of the Flix programming language. | |||
| Date | October 2020 | |||
| Report | CS-2020-05 (PDF) | |||
| CS-2020-06 | ||||
| Title | iDOT: A DOT Calculus with Object Initialization | |||
| Authors | Ifaz Kabir, Yufeng Li and Ondřej Lhoták | |||
| Abstract |
The
Dependent
Object
Types
(DOT)
calculus
serves
as
a
foundation
of
the
Scala
programming
language,
with
a
machine-verified
soundness
proof.
However,
Scala’s
type
system
has
been
shown
to
be
unsound
due
to
null
references,
which
are
used
as
default
values
of
fields
of
objects
before
they
have
been
initialized. This paper proposes iDOT, an extension of DOT for ensuring safe initialization of objects. DOT was previously extended to kDOT with the addition of mutable fields and constructors. To kDOT, iDOT adds an initialization effect system that statically prevents the possibility of reading a null reference from an uninitialized object. To design iDOT, we have reformulated the Freedom Before Commitment object initialization scheme in terms of disjoint subheaps to make it easier to formalize in an effect system and prove sound. Soundness of iDOT depends on the interplay of three systems of rules: a type system close to that of DOT, an effect system to ensure definite assignment of fields in each constructor, and an initialization system that tracks the initialization status of objects in a stack of subheaps. We have proven the overall system sound and verified the soundness proof using the Coq proof assistant. | |||
| Date | October 2020 | |||
| Report | CS-2020-06 (PDF) | |||
| CS-2020-07 | ||||
| Title | Handling Bidirectional Control Flow: Technical Report | |||
| Authors | Yizhou Zhang, Guido Salvaneschi and Andrew C. Myers | |||
| Abstract |
Pressed
by
the
difficulty
of
writing
asynchronous,
event-driven
code,
mainstream
languages
have
recently
been
building
in
support
for
a
variety
of
advanced
control-flow
features.
Meanwhile,
experimental
language
designs
have
suggested
effect
handlers
as
a
unifying
solution
to
programmer-defined
control
effects,
subsuming
exceptions,
generators,
and
async–await.
However,
despite
these
trends,
complex
control
flow
—
in
particular,
control
flow
that
exhibits
a
bidirectional
pattern
—
remains
challenging
to
manage.
We introduce bidirectional algebraic effects, a new programming abstraction that supports bidirectional control transfer in a more natural way. Handlers of bidirectional effects can raise further effects to transfer control back to the site where the initiating effect was raised, and can use themselves to handle their own effects. We present applications of this expressive power, which falls out naturally as we push toward the unification of effectful programming with object-oriented programming. We pin down the mechanism and the unification formally using a core language that makes generalizations to effect operations and effect handlers.The usual propagation semantics of control effects such as exceptions conflicts with modular reasoning in the presence of effect polymorphism — it breaks parametricity. Bidirectionality exacerbates the problem. Hence, we set out to show the core language, which builds on the existing tunneling semantics for algebraic effects, is not only type-safe (no effects go unhandled), but also abstraction-safe (no effects are accidentally handled). We devise a step-indexed logical-relations model, and construct its parametricity and soundness proofs. These core results are fully mechanized in Coq. While a full-featured compiler is left to future work, experiments show that as a first-class language feature, bidirectional handlers can be implemented efficiently. | |||
| Date | October 2020 | |||
| Report | CS-2020-07 (PDF) | |||