2020 technical reports

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)