16 citations · 19 across the 7 of their papers we have counts for
8 papers · 1 filter
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version)
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
Refinement types decorate types with assertions that enable automatic verification. Like assertions, refinements are limited to binders that are in scope, and hence, cannot express…
Refinement Types: A Tutorial
Ranjit Jhala, Niki Vazou
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable…
Learning to Blame: Localizing Novice Type Errors with Data-Driven Diagnosis
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri +2
Localizing type errors is challenging in languages with global type inference, as the type checker must make assumptions about what the programmer intended to do. We introduce Nate…
Deriving Law-Abiding Instances
Ryan Scott, Vikraman Choudhury, Ryan Newton +2
Liquid Haskell's refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. Bu…
Local Refinement Typing
Benjamin Cosman, Ranjit Jhala
We introduce the Fusion algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions…
Refinement Types for TypeScript
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
We present Refined TypeScript (RSC), a lightweight refinement type system for TypeScript, that enables static verification of higher-order, imperative programs. We develop a formal…