In the inaugural episode of Current Continuation, we talk to Prof. Ranjit Jhala of UCSD.
Ranjit has done influential work in program verification, including Lazy Abstraction and Liquid Types! He’s also incredibly nice and insightful.
Links

“PL Perspectives,” the SIGPLAN blog
Sinclair Spectrum
Ben Liblit
Thomas Henzinger
George Necula
Alex Aiken
Rupak Majumdar
2009 software model checking survey by Ranjit and Rupak
SPIN
VeriSoft
SLAM
Joseph Goguen
“Lazy Abstraction,” POPL 2002
Sriram Rajamani
“Liquid Types,” PLDI 2008
Hongwei Xi
Frank Pfenning
Dependent ML
Rust
Lean
Greg Morrisett
Mike Dodds
“N things I learned trying to do formal methods in industry,” a talk by Mike Dodds
“Flux: Liquid Types for Rust,” PLDI 2023
Flux on GitHub
Simon Peyton Jones
Verse
“The Verse Calculus: a Core Calculus for Functional Logic Programming,” ICFP 2023
Tim Sweeney
Jan Vitek
Sam Tobin-Hochstadt
David Van Horn
“Higher-Order Symbolic Execution for Contract Verification and Refutation,” JFP 2016
Liquid Haskell
Concrete Semantics
Isabelle
Software Foundations
Virginia Vassilevska Williams
Halide
“How to Design Talks”
“How to Design Programs”

Ver todos los episodios