University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Compiling Functional Types to Relational Specifications for Low Level Imperative Code

Compiling Functional Types to Relational Specifications for Low Level Imperative Code

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

  • UserNick Benton
  • ClockMonday 17 November 2008, 12:45-14:00
  • HouseFW26.

If you have a question about this talk, please contact Matthew Parkinson.

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple functional language into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and separation, over stores and values in the low-level machine.

This is joint work with Nicolas Tabareau from PPS , Paris 7.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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