Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:An Effectful Way to Eliminate Addiction to Dependence
Speaker:Pierre-Marie Pédrot
coming from:University of Ljubljana
Speakers Bio:
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Expert Audience
Language:English
Date, Time and Location
Date:Monday, 8 May 2017
Time:10:30
Duration:60 Minutes
Location:Saarbrücken
Building:E1 5
Room:029
Abstract

We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in
dependent type theory, such as exceptions, non-termination, non-determinism or writing operation. Through the light of a
call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially,
the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of
the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture
is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin.

Contact
Name(s):Brigitta Hansen
Phone:0681 93039102
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Meeting ID:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created:
Brigitta Hansen/MPI-SWS, 05/05/2017 04:05 PM
Last modified:
Uwe Brahm/MPII/DE, 05/08/2017 07:01 AM
  • Brigitta Hansen, 05/05/2017 04:08 PM -- Created document.