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.