BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Dependent Types and Fibred Computational Effects -
Danel Ahman\, University of Edinburgh\, Scotland
DTSTART;TZID=Europe/London:20160122T140000
DTEND;TZID=Europe/London:20160122T150000
UID:TALK62232AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/62232
DESCRIPTION:In this talk I will discuss the interplay between
two important topics in programming language resea
rch - dependent types and computational effects -
by presenting an effectful dependently-typed langu
age\, combining the features of Martin-Löf type th
eory and computational languages such as Call-By-P
ush-Value (CBPV) and the Enriched Effect Calculus
(EEC).\n\nSimilarly to CBPV and EEC\, our language
has both value types and terms and computation ty
pes and terms\, with both kinds of types only allo
wed to depend on value terms. By allowing the type
s to only depend on values\, we ensure that if a t
ype is to depend on an effectful computation\, it
has to exclusively happen via a thunk\, using only
the statically available information about the ef
fectful computation. A novel aspect of our languag
e is the use of computational sigma-types which we
use to account for type-dependency in the sequent
ial composition of computations.\n\nThe design of
our language is inspired and justified by a class
of categorical models we call fibred adjunction mo
dels. These naturally combine i) closed comprehens
ion categories arising from the semantics of depen
dent types\; and ii) adjunctions arising from the
semantics of computational effects. In the talk\,
I will present some examples of fibred adjunction
models based on the families fibration and adjunct
ions arising from the models of algebraic effects\
, e.g.\, state\, I/O\, exceptions\, etc.\; and fro
m the models of non-algebraic effects\, e.g.\, con
tinuations. I will also show how continuous famili
es of cpos can be used to give a semantics to an e
xtension of our language with general recursion.\n
\n(Joint work with Neil Ghani and Gordon Plotkin.)
LOCATION:FW26
CONTACT:Ohad Kammar
END:VEVENT
END:VCALENDAR