Participation #

ECLaPS took place on Saturday, October 4, 2025 at Université du Québec à Montréal (UQAM). There were twelve presentations and thirty-three attendees. Thanks to sponsorship from UQAM’s Computer Science Department, there was no cost to attend ECLaPS.

Schedule #

All regular talks are twenty minutes long followed by five minutes for questions. Several breaks are scheduled to encourage discussion between attendees.

9:15–9:30	Welcome
Session 0: Keynote Talk
9:30–10:25	Proto-Quipper: A family of functional programming languages for quantum computing.	Peter Selinger (Dalhousie University)
10:25–10:40	Break
Session 1: Logical Foundations
10:40–11:05	Ordered Adjoint Logic/Types	Sophia Roshal (Carnegie Mellon University)
11:05–11:30	Corps: A Core Calculus of Hierarchical Choreographic Programming	Andrew Hirsch (University at Buffalo, SUNY)
11:30–11:55	Simplicity: A first-order, finitary, functional language based on the Sequent Calculus	Russell O'Connor (Blockstream)
Lunch
11:55–13:30	Lunch @ Le Central (30 Sainte-Catherine West)
Session 2: Interoperability and Metaprogramming
13:30–13:55	Combining Functional Programming with Everything	Chuta Sano (McGill University)
13:55–14:20	Module Quotation and Ascription for Modular Macros	Maite Kramarz (University of Toronto)
14:20–14:30	Break
Session 3: Verification and Program Analysis
14:30–14:55	Cross-language Modelling of Effects - Java Exception into Dafny	Junyoung Jang (McGill University)
14:55–15:20	Blackbox Identification of Software Antivirus Features for Evasion with Software Probing	Philippe Pépos Petitclerc (UQAM)
15:20–15:45	Simplifying Dependent Reductions using Duality	Jonathon Yallop (Université de Montréal)
15:45–15:55	Break
Session 4: Mechanization and Proof Principles
15:55–16:20	McTT: A verified kernel for a proof assistant	Antoine Gaulin (McGill University)
16:20–16:45	Mechanizing linear logical relations	Daniel Zackon (McGill University)
16:45–17:10	Balance Contracts for Concurrent Trees	Hannah Gommerstadt (Vassar College)
17:10–17:15	Closing Remarks

Abstracts #

Proto-Quipper: A family of functional programming languages for quantum computing #

When I started working on quantum programming languages roughly 20 years ago, nobody in the quantum community cared about programming languages, and nobody in the programming language community knew much about quantum computing. Today, the situation is only marginally better: various labs are building quantum computers that are getting better every year, and many of them allow remote access, so programming quantum computers is something more and more people want to do in practice. However, they all want to use Python, and issues like strong typing, compositionality, or algebraic data types are far from the minds of most quantum programmers. On the other hand, quantum computing is notoriously difficult to do correctly and could probably benefit from things like formal verification.

The Proto-Quipper family of languages is our attempt at making a functional, strongly-typed language for quantum computing with well-defined operational and denotational semantics. I will report on our recent progress with these languages, and why it is surprisingly difficult to make them featureful enough to be truly practical.

Ordered Adjoint Logic/Types #

Ordered logic has been explored for a variety of use cases, including parsing, stream processing, and correctness guarantees. Our recent work on adjoint type systems introduced a mixed-mode type system assumes that all propositions at any mode are commutative. In this talk, we will present ongoing work to extend the adjoint type system to incorporate non-commutative modes.

So far, we have extended the adjoint sequent calculus with ordered modes, reformulating the standard rule of exchange as rules of mobility. Rather than viewing changes in order as exchanges between two propositions, we instead view them as movements of a single proposition. We have also established a cut elimination result for this sequent calculus.

Additionally, we have begun developing an algorithmic type checking system for the natural deduction formulation of this extended system. In addition to outlining our progress, this talk will discuss the challenges of designing such a system, and explore potential future directions.

Corps: A Core Calculus of Hierarchical Choreographic Programming #

Functional choreographic programming suggests a new propositions-as-types paradigm might be possible. In this new paradigm, communication is not modeled linearly; instead, ownership of a piece of data is modeled as a modality, and communication changes that modality. However, we must find an appropriate modal logic for the other side of the propositions-as-types correspondence. This paper argues for doxastic logics, or logics of belief. In particular, authorization logics—doxastic logics with explicit communication—appear to represent hierarchical choreographic programming. This paper introduces hierarchical choreographic programming and presents Corps, a language for hierarchical choreographic programming with a propositions-as-types interpretation in authorization logic.

Simplicity: A first-order, finitary, functional language based on the Sequent Calculus #

Simplicity is a little language based on the conjunctive-disjunctive fragment of the Sequent Calculus. It has sum and product types and a unit type. Simplicity has no recursion, nor recursive types. Simplicity comes with an abstract, two stack machine, called the Bit Machine, for evaluating Simplicity expressions. We model both the Simplicity language and the Bit Machine in the Rocq theorem prover and prove that well-typed Simplicity program execute correctly when interpreted with the Bit Machine. We can also bound the time and space costs of Simplicity programs in terms of the Bit Machine. Being a finitary language, Simplicity essentially expresses digital logic circuitry. Some possible applications of this language will be discussed.

Simplicity has been presented PLAS'17, and a paper is available at ⟨https://dl.acm.org/doi/pdf/10.1145/3139337.3139340⟩.

Combining Functional Programming with Everything #

There are many programming models and paradigms that are built and designed for particular domain-specific use cases. In particular, many languages and their implementations have varying tradeoffs between factors such as the static guarantees they offer, usage of runtime resources, etc. Further, there are languages that target beyond standard CPU chips, such as GPUs, custom architectures, and even quantum chips. “Real programming” often requires the combining of various programming paradigms, also known as interoperability, which, in practice, is achieved through very careful handwork.

In this talk, I propose adding a notion of first-class code based on contextual types to functional programming, enabling code generation, analysis, and execution. These codes capture programs in a suite of languages with differing syntaxes and operational semantics that the functional language can reason about. In particular, I apply this technique to a session-typed concurrency language, a low-level assembly-like language, and a quantum circuit language.

Module Quotation and Ascription for Modular Macros #

Ongoing work on modular macros has created a foundation for typed compile-time code generation, allowing programmers to write high-level code which generates efficient, low-level, and provably type-safe code. While existing research has shown how functors can be supported by this system, there are two important caveats:

1. 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.
2. Module ascription is not supported, as it can lead to scope extrusion of hidden values.

Although these do not seem to be very related problems, this talk will discuss how closure conversion and splitting can be used to overcome both issues in ways that are tightly intertwined.

Cross-language Modelling of Effects - Java Exception into Dafny #

Modelling a computational effect of one language in another language without the effect involves complex encoding, often unidiomatic and hardly readable to a human. Generating human-readable and idiomatic code is especially important when the source language provides stronger guarantees in mission-critical software at the cost of difficulties in learning or using the language and the target language is the opposite. In real-world applications, the difficulties of the source language blocks quick hot-fix, which is unavoidable for mission-critical software; for that, one needs to work on the target language, so the output should be readable, and preferably, idiomatic. When AWS rewrote AWS Identity, the initial gatekeeper for all AWS services, in Dafny for stronger guarantees, this was indeed the main concern. The long-lasting failure of AWS Identity would cause immeasurable damage on systems operating on AWS and AWS itself, so it needs hot-fix. However, there are not so many Dafny programmers in general, and the original version of AWS Identity was maintained by Java programmers. In order to utilize their pre-existing human resources, AWS Identity needs idiomatic Java, especially with its usual libraries using Java’s computational effects. One of such effects is exception, which Dafny does not support. In this talk, I will cover a way to model Java Exception in Dafny, and how it generates an idiomatic Java out of Dafny code. This work is a part of my AWS internship and published as a distinguished paper in ICSE 25: Chakarov et. al. Formally Verified Cloud-Scale Authorization.

Blackbox Identification of Software Antivirus Features for Evasion with Software Probing #

Red teaming and penetration testing are core practices of the cybersecurity audit landscape. Both of these practices frequently rely on the ability to execute offensive software tools that usually are detected as malicious by antivirus software. To achieve the execution of these tools on systems where antivirus software are installed, operators rely on several techniques to evade detection. In practice, detection evasion is usually ill-informed guesswork. A better methodology for evasion would allow for more efficient, and therefore more affordable campaigns and thus contribute towards more cyberresilient organisations. This presentation will discuss our ongoing research into methodologies for deducing information about antivirus engines present in software solutions as well as remaining complexities and the hurdles to obtaining informative data. Our approach relies on mapping the detection features of a given antivirus with different software probes, then deducing the required evasion techniques to apply in order to deliver and execute a payload. Correct identification of antivirus engine components would allow evasion techniques to be applied intently and minimally, reducing chances of unexpected detections and decreasing time spent on evading antivirus software.

Simplifying Dependent Reductions using Duality #

Reductions are operations which combine data together using an associative (and for our purposes, commutative) operator to produce a new collection of values. Oftentimes, reduction operations exhibit reuse and compute the same value multiple times, and this reuse can be optimized away. In simplifying dependent reductions, we discuss extensions to a preexisting simplification algorithm which enable the algorithm to optimize a larger class of programs, namely dependent reductions. These are reductions where the steps in our computation rely on one another. In this case, the original algorithm might use illegal simplifications, or optimizations that lead to invalid programs. Our extensions include a method for removing illegal simplifications from consideration, sufficient conditions for optimal simplification, and a heuristic for simplification selection when those conditions are not satisfied. For all of these extensions, we rely on the mathematical notion of duality, which enables us to unify a number of different aspects of the problem and consider them solely in terms of program dependences.

McTT: A verified kernel for a proof assistant #

Proof assistants based on type theories have been widely successful from verifying safety-critical software to establishing a new standard of rigour by formalizing mathematics. But these proof assistants and even their type-checking kernels are also complex pieces of software, and software invariably has bugs, so why should we trust such proof assistants? In this talk, I will describe the McTT (Mechanized Type Theory) infrastructure to build a verified implementation of a kernel for a core Martin-Löf type theory (MLTT). McTT is implemented in Rocq and consists of two main components: In the theoretical component, we specify the type theory and prove theorems such as normalization, consistency and injectivity of type constructors of MLTT using an untyped domain model. In the algorithmic component, we relate the declarative specification of typing and the model of normalization in the theoretical component with a functional implementation within Rocq. From this algorithmic component, we extract an OCaml implementation and couple it with a front-end parser for execution. This extracted OCaml code is comparable to what a skilled human programmer would have written and we have successfully used it to type-check a series of small-scale examples. McTT provides a fully verified kernel for a core MLTT with a full cumulative universe hierarchy. Every step in the compilation pipeline is verified except for the lexer and pretty-printer. As a result, McTT serves both as a first step to explore the meta-theory of advanced type theories and to investigate optimizations of and extensions to the type-checking kernel.

Mechanizing linear logical relations #

Logical relations (LR) are a powerful proof technique in programming language theory, but mechanizing them in proof assistants is often challenging. These difficulties are amplified in substructural settings (such as linear, affine, or relevant type systems), where contexts must be carefully managed as assumptions are split and consumed.

We describe how mechanized LR proofs can be adapted from intuitionistic to linear settings, highlighting the additional complexity introduced by linearity. We then propose an alternative based on approximate typing: embedding linear systems into purely structural calculi where standard logical relations suffice. This approach factors out the overhead of direct linear reasoning while still yielding key meta-theoretic results.

Balance Contracts for Concurrent Trees #

A concurrent system is a system where multiple processes collaborate on a computation. A concurrent contract represents a property of the computation that should remain true throughout the computation. Monitors can be used to check at runtime that a computation adheres to its contract. My work uses session types to monitor concurrent contracts. This talk will focus on various balancing contracts for split-join trees, which are widely used in a concurrent setting.