Type checking a garbage collector
Abstract: Static type checking is traditionally used for high level code. And indeed, low-level code often relies on properties which can be difficult to capture in type annotations. In this talk I will present the design of a generational garbage collector that can be type-checked to guarantee that it won't dereference dangling pointers and that it will preserve the type of the heap objects.
Type-preserving compilation in Haskell
Abstract: Type systems are the most widespread form of formal methods in wide use nowadays. Yet type checking only guarantees properties about the source code, after which we usually have to trust the compiler to preserve those properties. In this talk, I will show how we can use modern typing tools in a language like Haskell in order to write a compiler in such a way that type-checking the compiler verifies not only that no type error will occur during compilation, but also that it will preserve the typing properties of the programs it compiles.
Typer: an ML sibling inheriting from Lisp and Coq
Abstract: In this talk I will present the design of the programming language Typer that we are developing. Typer's core is very similar to proof assistants like Coq, so it support fully dependent types and lets you write and manipulate arbitrary propositions and proofs. Yet, being designed as a programming language more than a proof assistant, it pays more attention to issues such as performance and support for simple types.
Professor Stefan Monnier graduated in computer science from the EPFL, Switzerland, got his PhD from Yale University in 2003, and has been professor at the Université de Montréal since. He worked on the optimization phases of the typed intermediate language in SML/NJ, and spent more time than he wants to admit maintaining Emacs. His research focuses on the use of types for program verification, especially applied to compilers and memory management.