15 citations · 16 across the 3 of their papers we have counts for
4 papers
Efficiency of Learning from Proof Blocks Versus Writing Proofs
Seth Poulsen, Yael Gertner, Benjamin Cosman +2
Proof Blocks is a software tool that provides students with a scaffolded proof-writing experience, allowing them to drag and drop prewritten proof lines into the correct order inst…
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…
Trust, but Verify: Two-Phase Typing for Dynamic Languages
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
A key challenge when statically typing so-called dynamic languages is the ubiquity of value-based overloading, where a given function can dynamically reflect upon and behave accord…