Ranjit Jhala

In this episode, we talk to Dr. Satnam Singh who is a scientist at Groq. Zoom failed us and Adrian’s camera wasn’t captured in the recording. (It turns out that if you turn off “self view” in Zoom, that also turns off your video stream in the recording.) Links Groq Sinclair ZX80 Sinclair ZX Spectrum BBC Micro 6502 processor BBC BASIC Deutsches Elektronen-Synchrotron David Watt Ada Programmable Array Logic (PAL) Programmable logic array (PLA) Robin Milner Mary Sheeran Transputer Occam Miranda GHC Stephen Blott Satnam’s thesis, “Analysis of Hardware Descriptions” (1991) Verilog VHDL SystemVerilog Lava Bluespec I unfortunately couldn’t find a good link for John Gray. “Checking Safety Properties Using Induction and a SAT-Solver,” FMCAD 2000 Logical equivalence checking egg MLIR JasperGold Phil Wadler Simon Peyton Jones John Hughes John Launchbury Simon Marlow Graham Hutton Susan Spence and Persistent Java Bill Carter Satnam’s blog post, “Abuse and Bullying: An Ad Hoc Personal Survival Guide” Systolic array Ian Pratt XenSource Verilator YosysHQ Tobias Grosser Lean-MLIR Daniel Spoonhower Bob Harper Lindsey Kuper REACH conference Alastair Donaldson FP Castle Schloss Dagstuhl Brett NOPI Octomore

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”