登录
站内检索:
加拿大蒙特利尔大学的Stefan Monnier教授到软件开发环境国家重点实验室访问交流
加拿大蒙特利尔大学的Stefan Monnier教授到软件开发环境国家重点实验室访问交流
2016-08-20

2016年8月15日-23日,加拿大蒙特利尔大学的Stefan Monnier教授来实验室进行了访问交流,并围绕程序设计语言和编译中的类型保持问题做了三个学术报告。

报告的题目和摘要如下:

 

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.

 

报告的slides下载