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.
|