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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Compiling Functional Types to Relational Specifications for Low Level Imperative Code

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Average on weekdays: 9020.09571429 kWh Ryle Room, Kavli Solving Problems with Molecular Techniques

Other talks

Title TBC The uplift and erosion history of the Gamburtsev Subglacial Mountains and their role in the formation of the East Antarctic Ice Sheet Morning Break Non-stationarity in structural dynamics, challenges and implications for modelling and structural health monitoring Shape modes of CP^1 vortices Polar Oceans Seminar Talk
 

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