Linear dependent types: Complexity of PCF term evaluation.

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

• Barbara Petit, Università di Bologna
• Monday 11 June 2012, 14:00-15:00
• CS 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.

This talk is included in these lists:

• CS 217
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.