ETAPS 2019 (series) / DICE-FOPARA 2019 (series) / Workshop on Developments in Implicit Computational complExity & Foundational & Practical Aspects of Resource Analysis /
Finite semantics of polymorphism, complexity and the power of type fixpoints
Many applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We present two constructions of finite semantics for second-order Multiplicative-Additive Linear Logic (MALL2) and study their properties. We apply this to understand the gap in expressive power between MALL2 and its extension with type fixpoints, and to obtain an implicit characterization of regular languages in Elementary Linear Logic. Furthermore, some semantic results established here lay the groundwork for a sequel paper proposing a new approach to sub-polynomial implicit complexity.
Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 7 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:30 | |||
09:00 45mTalk | Finite semantics of polymorphism, complexity and the power of type fixpoints DICE-FOPARA Lê Thành Dũng Nguyễn , Thomas Seiller CNRS, Paolo Pistone University of Tübingen, Lorenzo Tortora de Falco | ||
09:45 45mTalk | From normal functors to logarithmic space queries DICE-FOPARA |