Dependent Types and Fibred Computational Effects

Add to your list(s) Download to your calendar using vCal

• Danel Ahman, University of Edinburgh, Scotland
• Friday 22 January 2016, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Ohad Kammar.

In this talk I will discuss the interplay between two important topics in programming language research – dependent types and computational effects – by presenting an effectful dependently-typed language, combining the features of Martin-Löf type theory and computational languages such as Call-By-Push-Value (CBPV) and the Enriched Effect Calculus (EEC).

Similarly to CBPV and EEC , our language has both value types and terms and computation types and terms, with both kinds of types only allowed to 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 information 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.

The design of our language is inspired and justified by a class of categorical models we call fibred adjunction models. These naturally combine i) closed comprehension categories arising from the semantics of dependent 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 adjunctions arising from the models of algebraic effects, e.g., state, I/O, exceptions, etc.; and from the models of non-algebraic effects, e.g., continuations. I will also show how continuous families of cpos can be used to give a semantics to an extension of our language with general recursion.

(Joint work with Neil Ghani and Gordon Plotkin.)

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.