Explicit Refinement Types

Ghalayini, JE; Krishnaswami, N

Ghalayini, JE (通讯作者),Univ Cambridge, Dept Comp Sci & Technol, Cambridge, England.

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023; 7 (ICFP):

Abstract

We present lambda(ert), a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver l......

Full Text Link