Séminaire
Le séminaire Langages et Logique Montréal (LLM) est un séminaire mensuel sur les langages de programmation et la logique. Il regroupe des participants de l’Université du Québec à Montréal, de l’Université de Montréal et de l’Université McGill. Il cherche à:
- Encourager l’échange sur la recherche en langages de programmation et en logique.
- Faciliter la collaboration entre les chercheurs à Montréal.
- Offrir un environnement informel pour permettre aux étudiants de présenter leurs travaux en cours.
Le format « colloquium » #
Les intérêts de la communauté montréalaise qui s’intéresse aux langages de programmation sont très variés et incluent des sujets tels que les fondements logiques et la sémantique catégorielle, l’analyse statique et la conception de compilateurs. Pour assurer que les présentations sont accessibles à l’entièreté de notre communauté, nous avons adopté le format « colloquium ». En particulier, le gros de chaque présentation doit être clair pour l’ensemble des étudiants de deuxième ou troisième cycles en informatique. L’article « How to give a good colloquium » de John McCarthy offre d’excellents conseils sur la préparation et l’exécution de telles présentations. Nos présentations sont généralement en anglais, mais elles peuvent se faire en français.
Durée #
Chaque réunion comprend une conférence invitée de 50 minutes (suivie de 10 minutes de questions) ou plusieurs exposés plus courts présentés par des étudiants. Le séminaire LLM a lieu tous les mois, généralement de 16 h à 17 h, et nous vous encourageons à vous joindre à nous pour un moment de convivialité après la réunion.
Si vous souhaitez présenter, veuillez contacter Ryan Kavanagh <kavanagh.ryan@uqam.ca>.
Liste de diffusion #
Pour recevoir des informations sur les présentations à venir, envoyez un courriel avec le contenu suivant à l’adresse <listserv@listserv.uqam.ca>:
subscribe LLM firstname lastname
Présentations passées et à venir #
30 avr. 2025
Aeneas: Formal Verification of Rust programs by Functional Translation
Orateur: Aymeric Fromherz (Inria)
Quand: le mercredi 30 avril 2025 de 16 h à 17 h
Où: PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy
Diapos: PDF
Résumé: 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.
31 mars 2025
Présentations étudiantes: Genesse, Huberdeau et Sano
MAPLS a été renommé à LLM: merci à Jean Privat pour la suggestion!
Orateurs: Hugo Genesse (UQAM), Laurent Huberdeau (Université de Montréal) et Chuta Sano (McGill University)
Quand: le lundi 31 mars 2025 de 16 h à 17 h
Où: PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy.
24 févr. 2025
Oratrice: Liron Cohen
Quand: le lundi 24 février 2025 de 16 h à 17 h
Où: PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy.
Résumé: 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.