Focusing on Refinement Typing

ACM Transactions on Programming Languages and Systems, 10.1145/3610408 (arXiv:2209.13000 [cs.PL])

Dimitrios J. Economou, Neel Krishnaswami and Jana Dunfield

Abstract

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

BibTeX entry

  @Article{Economou23,
    author =    {Dimitrios J. Economou and Neel Krishnaswami and Jana Dunfield},
    title =     {Focusing on Refinement Typing},
    journal =   {ACM Transactions on Programming Languages and Systems},
    year =      {2023},
    volume =    {45},
    number =    {4},
    pages =     {1--62},
    doi  =      {10.1145/3610408},
    note =      {\url{http://arxiv.org/abs/2209.13000}}
  }
  

all papers * related papers
J. Dunfield