Ontario Programming Languages Seminar
- Date
- Location
- McMaster University
About
The Ontario Programming Languages Seminar (ONPLS) is an informal gathering of programming languages researchers from across Ontario and neighboring areas. The focus is on sharing ideas, building community, encouraging discussion, and fostering collaboration.
- Organizers
- Program Committee
Talk Proposals
Talk proposals closed on (AoE). Acceptance emails have been sent.
Talk Guidelines
- Timing: 15 minutes for the presentation, followed by a 5 minute Q&A.
- Equipment: You may bring your own laptop or email us your slides 24 hours in advance to use one of ours.
Registration
Registration closed on (AoE).
Program
-
- Coffee
-
- Welcome
-
- Generating Human-Readable Code Jason Balaci, McMaster University
[Abstract]
Executable code often takes priority over documentation in software development. One inherent problem is knowledge duplication in code and documentation. Can we avoid that by generating everything? What would such a process look like?
This talk will discuss exploratory work in Drasil, a software generation framework for complete scientific software artifacts fit for humans, where we define "complete" as containing all software artifacts normally contained in a code repository (code, documentation, build scripts, etc.), and "fit for humans" as being well-documented and being idiomatic with meaningful identifiers.
The software generation pipeline in Drasil resembles a highly rational, explainable software development process. This talk will deconstruct said process, discussing: codifying problem-space concepts with domain-specific languages, refining problems into solutions through making concrete decisions about how problems should be translated into software artifacts.
-
- High-level Optimization of Abstract Data Types Anthony Hunt, McMaster University
[Abstract]
Sets, sequences, and relations are essential to describing system behaviours in formal specification and modelling languages like Event-B, Alloy, and Dafny. Conversely, high-level programming languages (like Python and Haskell) support only a subset of these types and operators, preferring the use of implementation-aware types like arrays and classes. In ongoing work, we use specification language semantics to enhance programming language performance. We propose a language capable of high-level expressions for abstract data types with efficient, guaranteed bounds for runtime and memory consumption; compilation is formulated as a series of provable term rewriting passes that closely follow set theory.
-
- Staging Module Functors Maite Kramarz, University of Toronto
[Abstract]
Ongoing work on MacoCaml has created a foundation for typed compile-time code generation, allowing programmers to write high-level code which generates efficient, specialized, and provably type-safe code. While existing research has shown how module functors can be supported in MacoCaml, code generation within functor bodies does not occur until application-time, even if the macros in the functor body do not depend on their argument. This talk will discuss how closure conversion and module splitting can be used to overcome this limitation, and arrive at a more unified theory of how code generation should operate in the presence of module functors.
-
- Borrowability as a Resource: A Core Calculus for Rust-Style Borrowing Yanning Chen, University of Toronto
[Abstract]
Rust is a systems programming language that provides memory safety without garbage collection. At the core of Rust is a combination of affine types and borrowing, allowing temporary transfers of resource permissions. This mechanism supports safe sharing and mutation without reference counting, and it avoids the explicit threading of resources through computation that is common in linear type systems. However, formalizing Rust's type system remains challenging. Existing formalizations often either fail to capture features such as non-lexical lifetimes, or rely on semantic side conditions.
In this talk, I will present a core type system for Rust-style borrowing. The key observation is that ownership can be viewed as the capability to introduce future borrows. Creating a borrow consumes part of this capability and leaves a residual resource that determines which future borrows remain available. I will then discuss ongoing work on a semantic model of the type system in separation logic.
-
- Coffee
-
- Record Types Everywhere Matthew Toohey, University of Toronto
[Abstract]
Modern functional programming languages, which build on the foundation of the lambda calculus, often adopt a substitution-based approach to variables. While this is a well-established convention, the use of substitution has some drawbacks. These include complexities with shadowing, which must be handled by formalizations in proof assistants, and efficiency issues that often result in significant differences between the theoretical model and practical implementations.
This talk will describe a language which takes an alternative approach by building on prior research into first-class environments. Using records to model environments allows many of the issues with substitution to be avoided while faciliating straightforward descriptions of useful operations on environments. This language also uses records to handle function arguments, which allows a variety of interesting function application features to be supported.
-
- Lessons from Mechanizing Categorical Logic in Cubical Agda Steven Schaefer, University of Michigan
[Abstract]
We present cubical-categorical-logic, a library of formalized category theory in Cubical Agda. The library’s core idea is to treat syntax as a free categorical structure whose dependent eliminator is stated via (displayed) universal properties. From the same reusable components we have proven canonicity and conservativity results across several type theories, as well as the coherence theorem for monoidal categories. In this talk, we discuss these applications and reflect on Cubical Agda as a host for mechanized metatheory, where it is sometimes a boon and sometimes a bane.
-
- Making Dynamic Language Object Encodings Matter Dave Mason, Toronto Metropolitan University
[Abstract]
In dynamically typed programming languages, variables and expressions do not have types associated with them; instead, values have types. This means that selecting the correct machine instructions to operate on data requires run-time dispatch based on the types associated with the values. The simplest encoding strategy is to store every object in a memory heap, where each object is tagged with its type. This approach places significant pressure on both the memory subsystem and the memory allocation system. At the other extreme, the most complex encoding strategies place as many values as possible into immediate representations to reduce this pressure. We describes a dozen different encoding strategies, ranging from all-memory representations to NaN-based encodings and evaluates their relative performance.
-
- Transitioning to Explicit Nulls in Scala: One Must Imagine Nullness Safety Harris Lau, University of Waterloo
[Abstract]
Null pointers have been described by its creator as the "billion dollar mistake". In this talk I will present the journey we took in Scala to transition from an implicitly nullable type system to an explicitly nullable one. Along the way we will explore the tradeoffs between correctness and compatibility, and the techniques we can use to close the gap as much as possible.
-
- Lunch
-
- Mikan: a New Proof Assistant for Cubical Type Theory Reed Mullanix, McMaster University
[Abstract]
We present Mikan, a new proof assistant for DeMorgan cubical type theory. In this talk I will provide a high-level motivation and overview of cubical type theory. I also discuss the high-level design goals of Mikan, challenges we have faced, and discuss possible future directions.
-
- Virtualizing Continuations Cong Ma, University of Waterloo
[Abstract]
Effect handlers and multishot continuations are powerful abstractions for managing control flow; together, they offer concise and modular ways to express and handle nondeterminism, randomness, and more. However, implementing multishot continuations in the presence of stack-allocated lexical resources—lexical effect handlers in particular—is challenging, since stack copying invalidates references to these resources.
In this talk, I will present a novel implementation strategy for lexical effect handlers that fully supports multishot continuations. The key idea is to virtualize the stack space used by continuations. Each stack-allocated handler instance is assigned a virtual address, and all effect invocations through these virtual addresses are mediated by an address translation mechanism. A software-based memory management unit in the runtime system performs these translations efficiently, exploiting the lexical scoping discipline of effect handlers.
We capture the essence of our approach via a new operational semantics for lexical effect handlers and prove it correct with respect to the standard semantics. We also implement it in a compiler and runtime system. Compared to prior languages with lexical effect handlers, our implementation increases expressivity by fully supporting multishot continuations—and, as a happy consequence, unlocks significant performance gains by enabling parallel execution of multishot continuations.
-
- Modules in C Alvin Zhang, University of Waterloo
[Abstract]
C's specification notably lacks a native module system, relying instead on ad-hoc techniques such as header files and translation units to achieve modularity. We investigate how C's unique position in systems programming makes it challenging to introduce modules, and investigate how other systems programming languages mitigate these problems. In particular, we look at C++20 modules and how its restriction on build order presents problems for migration efforts.
Through our analyses, we find that a specification for C modules that remains faithful to C programming patterns is achievable through partial parsing of top-level declarations. We demonstrate feasibility by implementing this module system in clang. We also take a closer look at design aspects such as restricting the preprocessor, avoiding grammar ambiguities, namespaces, inline functions, and handling initialization order.
-
- C∀ Container Library Peter Buhr, University of Waterloo
[Abstract]
All modern programming languages provide these three high-level containers (collections): array, linked-list, and string. Often, the array is part of the programming language, while linked lists are built from (recursive) pointer types, and strings from arrays and/or linked lists. For all three types, languages and/or their libraries supply varying degrees of high-level mechanisms for manipulating these objects at the bulk and component levels, such as copying, slicing, extracting, and iterating among elements. Unfortunately, typical implementations for the these key types in C cause 60%-70% of the reported software vulnerabilities involving memory errors, where 70%-80% of hacker attack-vectors target these types. As a result, C is under pressure from educators, industry, government, and the military. Therefore, hardening these three C types goes a long way to increase memory safety in the majority of C programs.
The new C∀ programming language strives to fix issues in C, chief among them safety. This talk describes improvements to the C∀ language design to support advanced container features, removing unsafe pointer operations. Specifically, an array is provided that tracks its length internally, relieving the user and implementor from managing explicit length arguments/parameters and stopping buffer-overrun errors. This feature requires augmenting the C∀ type system, making array length available at compile and runtime. A linked-list utility is provided that obviates many user-managed recursive pointers, while catering directly to system-programming using intrusive linking. A string utility is provided with implicit memory management of text in a specialized heap, removing error-prone buffer management, including overrun, and providing a copy-on-write speed boost. Finally, performance benchmarks show the new containers are on-par or surpass those in other comparable languages. These containers offer programmers workable alternatives to hand-rolling specialized libraries, which is a huge safety benefit, eliminating many system vulnerabilities.
-
- Coffee
-
- An Exercise in Proof Driven Software Understanding Joseph Tafese, University of Waterloo
[Abstract]
While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book. By combining large language models (LLMs), Prototype Verification System (PVS), and SeaHorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. In this seminar, we demonstrate how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.
-
- Effect Handlers in JAX Oghenevwogaga Ebresafe, University of Toronto
[Abstract]
JAX is a powerful machine learning framework that has driven recent advances in AI through efficient execution on hardware accelerators such as GPUs and TPUs. To achieve this performance, JAX requires programs to be written in a purely functional style. This restriction prevents the use of computational effects, forcing ML engineers to rely on complex workarounds to manage side effects.
We address this limitation by extending JAX with effect handlers. Because JAX uses a first-order intermediate representation without first-class functions or recursion, we develop a novel compilation approach for effectively translating effect handlers to target such a restricted language. We formalize the transformation process and prove semantics preservation in the Lean proof assistant. This design is implemented as an extension to JAX and we demonstrate its expressiveness through a case study in probabilistic programming.
-
- Choreographic Programming with Effect Handlers Max Jung, University of Waterloo
[Abstract]
Choreographic programming has been gaining interest as a programming paradigm for distributed systems. By writing a single, global “choreography” that is projected to local code at each endpoint automatically during compilation, this paradigm provides strong static guarantees about the projected programs. Most notably, any type-safe, projectable choreography is guaranteed to be deadlock-free. Recent works have been expanding the expressivity and capability of choreographic programs while preserving the static guarantees.
In this talk, we present our ongoing work on introducing effect handlers to choreographic programming, a powerful language mechanism that enables modular handling of computational effects and advanced control flows. We discuss how existing works on effect systems and endpoint projection can support effect handlers with minimal restrictions, while still preserving static guarantees such as deadlock freedom. By integrating effects and handlers, we can express programming patterns such as exception handling, streams, state abstractions, and simple transactions.
-
- Complete Local Reasoning About Parameterized Programs over Topologies Ruotong Cheng, University of Toronto
[Abstract]
We investigate the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness for them in the form of a universally quantified inductive invariant, where the quantification is over the nodes in the topology. We illustrate that under reasonable assumptions on the underlying topology, the problem can be reduced to and solved as a compositional scheme in which the verification of the parameterized family is reduced to a set of local proofs, in a complete manner. We propose a verification algorithm, which is implemented as a tool, and demonstrate through a set of benchmarks over several different topologies that our approach is effective in proving parameterized programs safe.
-
- Closing Remarks
Attending
- Venue
-
Room ITB A113. A map of ITB is available here.
Information Technology Building
McMaster University, 1280 Main St W, Hamilton, ON L8S 4L8
- Public Transit
- The most direct way to get to McMaster via public transit is to take the Go bus to the McMaster University bus terminal. It is also possible to take the Go train to either the Hamilton GO Centre or West Harbour GO, and then take the HSR Route 10 - B Line Express to McMaster. All listed options accept Presto cards.
- Visitor Parking
- For more information, see Visitor Parking.
Contact
- Reed Mullanix
- mullanir@mcmaster.ca
- Jason Balaci
- balacij@mcmaster.ca