University of Birmingham > Talks@bham > Lab Lunch > Linear dependent types: Complexity of PCF terms evaluation

Linear dependent types: Complexity of PCF terms evaluation

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

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

Joint Lab-Lunch and Theory Seminar

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 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 talks.cam from the University of Cambridge.