## Towards a propositional refinement type system for algebraic effects

School of Informatics

University of Edinburgh

Monday, 10 March 2014, 14:00 (notice the unusual weekday!)

Cybernetica Bldg (Akadeemia tee 21), room B101

**Abstract**: We present recent work on investigating an
algebraic treatment of propositional refinement types for languages
with computational effects. Our goal is to develop a refinement-typed
version of the call-by-push-value (CBPV) metalanguage to cover various
examples in a single system, such as Hoare Logic, communication
sessions, correct use of files, and effect set annotations, as found
in type-and-effect systems.

We present a type system with mutually defined computation and
value refinement types. Our work draws inspiration from a semantic
analysis involving fibrations and fibred adjunctions. The former
include specifications on computations by sets of algebraic terms, via
a fragment of the modal μ-calculus with a key role played by
diamond modalities indexed by algebraic operation symbols, called
operation modalities. Categorically such modalities correspond to
op-reindexing functors along the algebraic operations on algebras
denoting CBPV computation types. We axiomatize the logic involved in
refinement types as mutually defined sub-typing relations;
categorically as the internal logic of fibres over CBPV types.

Unfortunately, the semantic analysis does not validate all the
desired sub-typing rules. The reason is that not every equation in the
algebraic theory at hand does not give rise to corresponding two
sub-typing inequalities. We propose two ways to circumvent this
problem, neither being perfect. In the first approach, we add to the
rule for including algebraic equations in the sub-typing relations a
linearity constraint. This, however, forces us to strengthen the
typing rule for algebraic operations to involve arbitrary algebraic
terms and algebraic equations, to type all computation terms of
interest. In the second approach, we replace operation modalities with
diamond modalities indexed by terms from the algebraic theory at
hand. In this way, every algebraic equation induces the expected two
sub-typing inequalities. There is also an elegant semantic description
of such modalities, as a colax and linearly lax action of the abstract
clone of the algebraic theory on computation refinement
types. Unfortunately, this change introduces unnecessary redundancies
in the grammar of refinement-typed computation terms.

This is joint work with Gordon Plotkin.

Tarmo Uustalu

Last update 25.2.2014