Focusing on Liquid Refinement Typing

Unpublished manuscript

Dimitrios J. Economou, Neelakantan R. Krishnaswami and Jana Dunfield


We present a foundation systematizing, in a way that works for any evaluation order, the variety of mechanisms for SMT constraint generation found in index refinement and liquid type systems. Using call-by-push-value, we design a polarized subtyping relation allowing us to prove that our logically focused typing algorithm is sound, complete, and decidable, even in cases seemingly likely to produce constraints with existential variables. We prove type soundness with respect to an elementary domain-theoretic denotational semantics. Soundness implies, relatively simply, our system's totality and logical consistency.

arXiv version 1

BibTeX entry

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

all papers * related papers
J. Dunfield