Focusing on Index Refinement Typing

To appear in Transactions on Programming Languages and Systems

Dimitrios J. Economou, Neel Krishnaswami and Jana Dunfield


We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, the variety of mechanisms for SMT constraint generation seen in index refinement and liquid type systems for functional programming languages. By carefully combining a focalized variant of call-by-push-value, bidirectional typing, and our novel technique of value-determined indexes, our system generates solvable SMT constraints without existential (unification) variables. We design a polarized subtyping relation allowing us to prove our logically focused typing algorithm is sound, complete, and decidable. We prove type soundness of our declarative system with respect to an elementary domain-theoretic denotational semantics. Type soundness implies, relatively simply, the total correctness and logical consistency of our system. The relative ease with which we obtain both algorithmic and semantic results ultimately stems from the proof-theoretic technique of focalization.

arXiv version 1

BibTeX entry

    author =    {Dimitrios J. Economou and Neel Krishnaswami and Jana Dunfield},
    title =     {Focusing on Index Refinement Typing},
    month =     sep,
    year =      {2022},
    note =      {\url{}}

all papers * related papers
J. Dunfield