Dependent Types and Fibred Computational Effects

Daniel Ahman, Neil Ghani, Gordon D. Plotkin

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We study the interplay between dependent types and general computational effects. We define a language with both value types and terms, and computation types and terms, where types depend only on value terms. We use computational Σ-types to account for
type-dependency in the sequential composition of computations. Our language design is justified by a natural class of categorical models called fibred adjunction models. We show how to account for both algebraic effects and non-algebraic effects. We also show how to extend the language with general recursion, using continuous families of cpos.
Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publication19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages19
ISBN (Electronic)978-3-662-49630-5
ISBN (Print)978-3-662-49629-9
Publication statusPublished - Mar 2016
Event19th International Conference of Foundations of Software Science and Computation Structures - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference19th International Conference of Foundations of Software Science and Computation Structures
Abbreviated titleFOSSACS 2016
Internet address

Fingerprint Dive into the research topics of 'Dependent Types and Fibred Computational Effects'. Together they form a unique fingerprint.

Cite this