Current Continuation

Ranjit Jhala

Listen Later

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”
    • ...more
    View all episodesView all episodes
    Download on the App Store
    Current ContinuationBy Aws Albarghouthi and Adrian Sampson