Dependent Types and Fibred Computational Effects

Daniel Ahman, Neil Ghani, Gordon D. Plotkin

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

Abstract

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
Pages36-54
Number of pages19
ISBN (Electronic)978-3-662-49630-5
ISBN (Print)978-3-662-49629-9
DOIs
Publication statusPublished - Mar 2016
Event19th International Conference of Foundations of Software Science and Computation Structures - Eindhoven, Netherlands
Duration: 2 Apr 20168 Apr 2016
https://www.etaps.org/index.php/2016

Publication series

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

Conference

Conference19th International Conference of Foundations of Software Science and Computation Structures
Abbreviated titleFOSSACS 2016
CountryNetherlands
CityEindhoven
Period2/04/168/04/16
Internet address

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

Cite this