Colloquium
The LLM Colloquium is a monthly research talk series about programming languages and logic. It is jointly held between Université du Québec à Montréal (UQAM), Université de Montréal and McGill University. It seeks to:
- Facilitate the exchange of recent and ongoing work on programming languages and logic.
- Foster collaboration between researchers in Montreal.
- Give students a welcoming venue to present their ongoing work.
- Provide a venue for external speakers who wish to reach a broad cross-section of the Montreal programming languages and logic community.
Colloquium Format #
Montreal’s programming languages community is broad, ranging from type theory and categorical semantics, to static analysis and compiler design. To ensure that talks are accessible to the community as a whole, LLM has adopted a colloquium format. In particular, the majority of each talk should be broadly accessible to all computer science graduate students. John McCarthy’s How to give a good colloquium provide excellent advice on preparing colloquium talks.
Timing #
Each meeting features a 50 minute invited talk (followed by 10 minutes of questions), or several shorter student talks. The LLM Colloquium occurs monthly, typically from 16:00 to 17:00, and we encourage participants to join us for a social hour afterwards.
Speakers who are interested in presenting are invited to contact Ryan Kavanagh <kavanagh.ryan@uqam.ca>.
Talk announcements #
To subscribe to our low-volume announcement list, send an email with the following body to <listserv@listserv.uqam.ca>:
subscribe LLM firstname lastname
Talk schedule #
30 Apr 2025
Aeneas: Formal Verification of Rust programs by Functional Translation
Speaker: Aymeric Fromherz (Inria)
When: Wednesday, April 30 2025, 16:00–17:00
Where: Room PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy
Slides: PDF
Abstract: The Rust programming language has recently gained traction in industrial settings and in the systems community. A large part of this success stems from several key features of the language: Rust provides both the high performance and low-level idioms commonly associated to languages like C and C++, as well as memory safety by default thanks to its rich, borrow-based type system. However, despite being safer than C or C++, Rust programs are not immune to bugs and vulnerabilties, including aborted executions (i.e., Rust’s panic), incorrect uses of the unsafe escape hatch, or simply programs that do not match their expected behaviour, raising the need for novel static analyzers and verification tools.
To this end, we present Aeneas, a new toolchain geared towards the formal verification of Rust programs. Aeneas leverages Rust’s region-based type system to eliminate memory reasoning for a large class of Rust programs: relying on a custom borrow-centric symbolic execution, the toolchain translates safe Rust programs to a semantically equivalent functional model in proof assistants such as Lean, Rocq, or F*, enabling the use of powerful logics to specify and reason about programs.
In this talk, we will show the core ideas behind Aeneas’ functional translation on several examples, and present the broader ecosystem around Aeneas, including the Charon analysis framework and ongoing work on transpilers between C and Rust to handle legacy systems.
31 Mar 2025
Student talks: Genesse, Huberdeau and Sano
MAPLS has been rebranded to LLM: thanks to Jean Privat for the suggested rebranding!
Speakers: Hugo Genesse (UQAM), Laurent Huberdeau (Université de Montréal) and Chuta Sano (McGill University)
When: Monday, March 31 2025, 16:00–17:00
Where: Room PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy.
24 Feb 2025
Please join us for the first MAPLS seminar talk!
Title: Effectful Curry-Howard
Speaker: Liron Cohen
When: Monday, February 24 2025, 16:00–17:00
Where: Room PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy.
Abstract: The Curry-Howard correspondence and its semantic embodiment in the form of realizability, establish a foundational connection between logic, programming, and type systems. However, these fundamental frameworks fall short of addressing modern computational paradigms that rely on effects such as state, concurrency, and probabilistic behavior. This talk explores effectful Curry-Howard, focusing on extending the Curry-Howard correspondence to integrate computational effects into the framework of realizability. We introduce two new algebraic structures: Evidenced Frames, which provide an abstract structure for building effectful realizability models, and Monadic Combinatory Algebras, a monadic-based extension of traditional partial combinatory algebras. We will see how these extensions not only have a critical impact on the resulting theory, allowing novel computational interpretations of key principles, but also offer a robust framework for verifying modern computational systems.