University of Birmingham > Talks@bham > Theoretical computer science seminar > Linear dependent types: Complexity of PCF term evaluation.

Linear dependent types: Complexity of PCF term evaluation.

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

  • UserBarbara Petit, Universit√† di Bologna
  • ClockMonday 11 June 2012, 14:00-15:00
  • HouseCS 217.

If you have a question about this talk, please contact Paul Levy.

Joint Theory Seminar and Lab Lunch

Linear dependent types bring together the ideas of Bounded Linear Logic with the simulation of the lambda calculus in a linear setting, in order to capture the type complexity of functional programs. Ugo Dal Lago and Marco Gaboardi proposed (in LICS ’11) such a type system for PCF terms, that guarantees the correctness of the extensional behaviour of programs but also provides a precise complexity bound for their call-by-name evaluation. In this talk, we will see how this type system is related to the call-by-name translation of the simply typed lambda-calculus into linear logic (that is well known since the mid 90’s). We will then look at the corresponding call-by-value translation, and see how we can define a type system capturing the complexity of the call-by-value evaluation of PCF terms.

This talk is part of the Theoretical computer science seminar 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.