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

## Linear dependent types: Complexity of PCF terms evaluationAdd to your list(s) Download to your calendar using vCal - Barbara Petit, Bologna
- Monday 11 June 2012, 14:00-15:00
- CS 217.
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. ## This talk is included in these lists:- CS 217
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Lab Lunch
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsAnalysis Seminar Analysis Reading Seminar Computer Science Distinguished Seminar## Other talksTBC |