Dependent Types and Effects

Dependent types are types that refer to terms such as numbers and strings.  Such types enables us to precisely express specifications of programs.  However, most dependently typed languages do not allow effectful programs involving exception handling, destructive assignment, and so on.

In this project, we design a dependently typed language with support for a wide range of effects.  So far, Cong has given a dependent type system for delimited control operators, which are a tool for manipulating control flow of programs.  The idea is to maintain soundness of the type system by restricting types to depend only on non-effectful terms.

As future work, we intend to extend the type system with algebraic effects and handlers, and implement a prototype language based on that type system.

Members

News