POSTPONED: Abstract machines and certified compilers

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

• Maciej Piróg
• Thursday 17 September 2015, 10:00-11:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.