School of Informatics
University of Edinburgh
Thursday, 28 May 2015, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B126
Abstract: In this talk I will describe the syntax and semantics of a dependently-typed version of Levy's call-by-push-value (CBPV) programming language.
Those familiar with effectful programming know that a central construct in such languages is that of sequential (monadic) composition. The same also applies when one wants to equip the language with dependent types. I will begin by reviewing some of the attempts people have made to accommodate type-dependency into sequential composition. Then I will present the central idea of this work, drawing heavily on the algebraaic treatment of computational effects, of using coproducts of algebras to accommodate type-dependency in sequential composition. This in turn leads us to adding a type of dependent tensors to CBPV, moving the syntax closer to that of the enriched effect calculus (EEC) of Egger, Møgelberg and Simpson.
In addition to the dependently-typed calculus, I will also present its categorical models, based on closed comprehension categories and fibred adjunctions. Interestingly, it turns out that by moving from simple types to dependent types, one is able to axiomatize sthe structures in the models (including tensors, cotensors and strength) in standard (fibred) category theory, without having to appeal to enrichment or local indexing.
This is joint work with Neil Ghani and Gordon Plotkin.