University of Cambridge > Talks.cam > REMS lunch > POSTPONED: Abstract machines and certified compilers

POSTPONED: Abstract machines and certified compilers

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

A compiler is called certified if it comes with a machine-verified proof of its correctness with respect to the semantics of the source and target languages. In am going to talk about certified compilers for high-level languages with non-trivial semantics, such as the lazy semantics of Haskell, and how systematic manipulation of semantics can guide the design of such a compiler, or even automatise the process.

This talk is part of the REMS lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity