University of Birmingham > Talks@bham > Lab Lunch > Call-by-Value in a Basic Logic for Interaction

Call-by-Value in a Basic Logic for Interaction

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

  • UserSpeaker to be confirmed
  • ClockWednesday 12 November 2014, 15:00-16:00
  • HouseCS 222.

If you have a question about this talk, please contact Dan Ghica.

In game semantics and related approaches to programming language semantics, programs are modelled by interaction dialogues. Such models have been used by a number of authors for the design of compilation methods, in particular for applications where resource control is important. The work in this area has focused on call-by-name languages. This talk considers the compilation of call-by-value into a first-order low-level language by means of an interpretation in an interactive model. We work with the structure of the interactive model in terms of a typed calculus that can be seen as a fragment of Linear Logic. The main result is that Plotkin’s call-by-value CPS -translation and its soundness proof can be refined to target this intermediate language. This refined CPS -translation amounts to a direct compilation of the source language into a first-order low-level language.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.