|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|
|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|
|Title||A Semantics for the Essence of React|
|Authors||Magnus Madsen, Ondřej Lhoták and Frank Tip|
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|
|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|
|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.
|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.
|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.