Stefan Monnier

Professeur agrégé (associate professor)
Université de Montréal
Département d'informatique et de recherche opérationnelle
C.P. 6128, succ. centre-ville
Montréal, QC, H3C 3J7
Tel: ++1 (514) 343-6111 x47617
Fax: ++1 (514) 343-5834
Bureau: 2341, pavillon André-Aisenstadt

For courier, use: 2920, Chemin de la Tour #2194
Montréal, QC, H3T 1J4


Études supérieures.

Research Interests

I am interested in the design and implementation of strongly typed programming languages. I see a future where all programming is done in type safe languages or in assembly supplemented with safety proofs.

I am also interested in investigating what such a future means in terms of how we distribute the work between compilers, runtime systems, operating systems and computer architecture.

My main focus of research until now has for this reason been at the intersection between type-safety and memory-management which, from a programming-language point of view, is the most important part of the runtime system and the operating system.



I was maintainer of Emacs for quite a few years, so most of my contributions are included in there.


The bastard child of ML+Scheme+Coq: A programming language of the ML family, but inspired by Scheme's minimalism and syntactic structure and built on top of a pure λ-calculus with dependent types, similar to Coq's.


A distributed Issue Tracking System that builds on Git and aims to really let Issues live their own decentralized lives.

Professional activities

Programming Languages meets Program Verification (PLPV'07) workshop, colocated with ICFP'07 (program committee member).

Together with fellow researchers, I instigated the Québec Programming Languages Seminaire.

Collaboration with the Logic and Computation group at McGill.

Inference of class relationships in Java for UML-like models, together with Yann-Gaël Guéhéneuc.

Typing the implementation of various object oriented mechanisms, together with Chris League.

Working on garbage-collectors, with Marc Feeley.


Closure Converting the Universe. ?? and Stefan Monnier. draft.

Resizing Prop down to an axiom. Stefan Monnier. TYPES'2022 (draft).

Open Closures: Disclosing lambda's inner monomaniac object!. Stefan Monnier. ELS'2022.

Moebius: Metaprogramming using Contextual Types. Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka. POPL'2022.

Turbo BinDat: data is not code, Talk I gave at EmacsConf'21.

Computation over partial information, Ian Sabourin, Stefan Monnier, et Marc Feeley. IFL-2021 draft.

Is Impredicativity Implicitly Implicit?. Stefan Monnier et Nathaniel Bos. TYPES-2019 post-proceedings.

SMIE: Weakness is Power! Auto-indentation with incomplete information. Stefan Monnier. ⟨Programming⟩ 2020.

Evolution of Emacs Lisp. Stefan Monnier and Michael Sperber. HOPL'2020. (translated to Chinese)

Inductive types deconstructed: the calculus of united constructions. Stefan Monnier. TyDe'2019.

Typer: ML boosted with type theory and Scheme. Stefan Monnier. JFLA'2019.

Typer: An infix statically typed Lisp (extended abstract, slides). Pierre Delaunay, Vincent Archambault-Bouffard, and Stefan Monnier. ML'2017.

Implementation of Explicit Substitutions: from λσ to the Suspension Calculus. Vincent Archambault-Bouffard and Stefan Monnier. HOR'2016.

Programming type-safe transformations using higher-order abstract syntax. Olivier Savary-Belanger, Stefan Monnier, and Brigitte Pientka. JFR, 2015 (an extended and revised version of the CPP'13 paper).

Programming type-safe transformations using higher-order abstract syntax. Olivier Savary-Belanger, Stefan Monnier, and Brigitte Pientka. CPP'13.

Compiling Contextual Objects: Bringing Higher-Order Abstract Syntax to Programmers. Francisco Ferreira, Brigitte Pientka, and Stefan Monnier. PLPV'2013.

Singleton types here, Singleton types there, Singleton types everywhere. Stefan Monnier and David Haguenauer. PLPV'2010. (local copy)

Type invariants for Haskell. Tom Schrijvers, Louis-Julien Guillemette, and Stefan Monnier. PLPV'2009.

Statically tracking state with Typed Regions. Stefan Monnier. Unpublished, 2008.

One Vote for Type Families in Haskell!. Louis-Julien Guillemette and Stefan Monnier. TFP'08.

A Type-Preserving Compiler in Haskell. Louis-Julien Guillemette and Stefan Monnier. ICFP'08.

The Swiss Coercion. Stefan Monnier. PLPV'07.

A Type-Preserving Closure Conversion in Haskell. Louis-Julien Guillemette and Stefan Monnier. Haskell'07.

Concurrency Oriented Programming in Termite Scheme. Guillaume Germain, Marc Feeley, and Stefan Monnier. Scheme'06.

Statically Verified Type-Preserving Code Transformations in Haskell. Louis-Julien Guillemette and Stefan Monnier. PLPV'06.

Typed Compilation Against Non-Manifest Base Classes. Christopher League and Stefan Monnier. CASSIS'06, LNCS 3956.

Typed Regions. Stefan Monnier and Zhong Shao. YALEU/DCS/TR-1242, October 2002.

Principled Compilation and Scavenging. Stefan Monnier. PhD Thesis, July 2003. Also available as DVI.

Principled Scavenging. Stefan Monnier, Bratin Saha, and Zhong Shao. In Proc. 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01), Snowbird, UT, pages 81-91, June 2001. ©2001 ACM.

Inlining as Staged Computation. Stefan Monnier and Zhong Shao. In Journal of Functional Programming, volume 13(3), pages 647-676, May 2003.

A Syntactic Approach to Foundational Proof-Carrying Code (Extended Version). Nadeem Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. In Journal of Automated Reasoning, Volume 31, Issue 3-4, pages 191-229, 2003.

A Syntactic Approach to Foundational Proof-Carrying Code. Nadeem Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), Copenhagen, Denmark, pages 89-100, July 2002.

Mise en oeuvre d'un processeur de type SMT. Dominik Madon, Eduardo Sanchez, et Stefan Monnier. In Technique et Science Informatique, Volume 20 no1, pages 31-52, 2001.

A Study of a Simultaneous Multithreaded Architecture. Dominik Madon, Eduardo Sanchez, and Stefan Monnier. In Proc. EuroPar'99, Toulouse, Lecture Notes in Computer Science, Volume 1685, Springer-Verlag, pages 716-726, September 1999.

Implementing Typed Intermediate Languages. Zhong Shao, Christopher League, and Stefan Monnier. In Proc. 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP'98), Baltimore, Maryland, pages 313-323, September 1998. ©1998 ACM.

Previous occupation

While doing my PhD research at Yale, I spent time organizing for GESO and hacking on Emacs (including a few elisp packages, all of which are now bundled with Emacs, except for sml-mode).

My background is supposedly outlined in the Curriculum Vitae I used when looking for a job, but you might also want to check my home village's web page (as I said, it's a village, so don't expect too much). The site used to have nice pictures where (if you knew the place), you could recognize some buildings like the ones of the banks which manage the spare change of the world's tyrants (makes me wonder: does W have a swiss bank account?).