Encoding Tight Typing in a Unified Framework

Abstract: This joint work with Delia Kesner explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a tight type system for CBPV. All such systems are quantitative, in the sense that they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of sequences to normal forms are discriminated according to their multiplicative/exponential nature, a concept inherited from linear logic.

Spanishlogic in computer scienceprogramming languages

Audience: researchers in the topic

LoReL Seminar

Series comments: Talks are either in Spanish or English, however they can often be in English upon request.