BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Dependent Types and Fibred Computational Effects - Danel Ahman\, U
 niversity of Edinburgh\, Scotland
DTSTART:20160122T140000Z
DTEND:20160122T150000Z
UID:TALK62232@talks.cam.ac.uk
CONTACT:Ohad Kammar
DESCRIPTION:In this talk I will discuss the interplay between two importan
 t topics in programming language research - dependent types and computatio
 nal effects - by presenting an effectful dependently-typed language\, comb
 ining the features of Martin-Löf type theory and computational languages 
 such as Call-By-Push-Value (CBPV) and the Enriched Effect Calculus (EEC).\
 n\nSimilarly to CBPV and EEC\, our language has both value types and terms
  and computation types and terms\, with both kinds of types only allowed t
 o depend on value terms. By allowing the types to only depend on values\, 
 we ensure that if a type is to depend on an effectful computation\, it has
  to exclusively happen via a thunk\, using only the statically available i
 nformation about the effectful computation. A novel aspect of our language
  is the use of computational sigma-types which we use to account for type-
 dependency in the sequential composition of computations.\n\nThe design of
  our language is inspired and justified by a class of categorical models w
 e call fibred adjunction models. These naturally combine i) closed compreh
 ension categories arising from the semantics of dependent types\; and ii) 
 adjunctions arising from the semantics of computational effects. In the ta
 lk\, I will present some examples of fibred adjunction models based on the
  families fibration and adjunctions arising from the models of algebraic e
 ffects\, e.g.\, state\, I/O\, exceptions\, etc.\; and from the models of n
 on-algebraic effects\, e.g.\, continuations. I will also show how continuo
 us families of cpos can be used to give a semantics to an extension of our
  language with general recursion.\n\n(Joint work with Neil Ghani and Gordo
 n Plotkin.)
LOCATION:FW26
END:VEVENT
END:VCALENDAR