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 - 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. |
## Other listsHuman Computer Interaction seminars Centre for Computational Biology Seminar Series Bham Talks## Other talksView fusion vis-à-vis a Bayesian interpretation of Black-Litterman for portfolio allocation TBC How to stratify PSPACE-complete logics into fragments complete for each level of the polynomial time hierarchy? TBC Advancing biomedical photoacoustic imaging using structured light and optical microresonators Structured Decompositions: recursive data and recursive algorithms |