Ranjit Jhala

Satnam Singh

In this episode, we talk to Dr. Satnam Singh [https://raintown.org] who is a scientist at Groq [https://groq.com]. 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 [https://groq.com] * Sinclair ZX80 [https://en.wikipedia.org/wiki/ZX80] * Sinclair ZX Spectrum [https://en.wikipedia.org/wiki/ZX_Spectrum] * BBC Micro [https://en.wikipedia.org/wiki/BBC_Micro] * 6502 processor [https://en.wikipedia.org/wiki/MOS_Technology_6502] * BBC BASIC [https://en.wikipedia.org/wiki/BBC_BASIC] * Deutsches Elektronen-Synchrotron [https://en.wikipedia.org/wiki/DESY] * David Watt [http://www.dcs.gla.ac.uk/people/personal/daw/] * Ada [https://en.wikipedia.org/wiki/Ada_(programming_language)] * Programmable Array Logic (PAL) [https://en.wikipedia.org/wiki/Programmable_Array_Logic] * Programmable logic array (PLA) [https://en.wikipedia.org/wiki/Programmable_logic_array] * Robin Milner [https://en.wikipedia.org/wiki/Robin_Milner] * Mary Sheeran [https://www.cse.chalmers.se/~ms/] * Transputer [https://en.wikipedia.org/wiki/Transputer] * Occam [https://en.wikipedia.org/wiki/Occam_(programming_language)] * Miranda [https://en.wikipedia.org/wiki/Miranda_(programming_language)] * GHC [https://www.haskell.org/ghc/] * Stephen Blott [https://www.dcu.ie/computing/people/stephen-blott] * Satnam’s thesis, “Analysis of Hardware Descriptions” (1991) [https://theses.gla.ac.uk/78311/] * Verilog [https://en.wikipedia.org/wiki/Verilog] * VHDL [https://en.wikipedia.org/wiki/VHDL] * SystemVerilog [https://en.wikipedia.org/wiki/SystemVerilog] * Lava [https://raintown.org/lava/] * Bluespec [https://github.com/B-Lang-org/bsc] * I unfortunately couldn’t find a good link for John Gray. * “Checking Safety Properties Using Induction and a SAT-Solver,” [https://dl.acm.org/doi/10.5555/646186.683237] FMCAD 2000 * Logical equivalence checking [https://en.wikipedia.org/wiki/Formal_equivalence_checking] * egg [https://egraphs-good.github.io] * MLIR [https://mlir.llvm.org] * JasperGold [https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification.html] * Phil Wadler [https://homepages.inf.ed.ac.uk/wadler/] * Simon Peyton Jones [https://simon.peytonjones.org] * John Hughes [https://www.cse.chalmers.se/~rjmh/] * John Launchbury [https://launchbury.blog] * Simon Marlow [https://simonmar.github.io] * Graham Hutton [https://people.cs.nott.ac.uk/pszgmh/] * Susan Spence and Persistent Java [https://www.semanticscholar.org/paper/Design-Issues-for-Persistent-Java%3A-A-Type-Safe%2C-Atkinson-Jordan/436e8238492ede8329a26d10539d59c6aead1018] * Bill Carter [https://www.scu.edu/engineering/about/engineering-advisory-board/eab-profiles/carter.html] * Satnam’s blog post, “Abuse and Bullying: An Ad Hoc Personal Survival Guide” [https://raintown.org/abuse/] * Systolic array [https://en.wikipedia.org/wiki/Systolic_array] * Ian Pratt [https://en.wikipedia.org/wiki/Ian_Pratt_(computer_scientist)] * XenSource [https://wiki.xenproject.org/wiki/XenSource] * Verilator [https://www.veripool.org/verilator/] * YosysHQ [https://www.yosyshq.com] * Tobias Grosser [https://www.cst.cam.ac.uk/people/tcg40] * Lean-MLIR [https://github.com/opencompl/lean-mlir] * Daniel Spoonhower [https://www.cs.cmu.edu/~spoons/] * Bob Harper [https://www.cs.cmu.edu/~rwh/] * Lindsey Kuper [https://decomposition.al] * REACH conference [https://reach.theiet.org] * Alastair Donaldson [https://www.doc.ic.ac.uk/~afd/] * FP Castle [https://fpcastle.com] * Schloss Dagstuhl [https://www.dagstuhl.de] * Brett [https://www.brettrestaurant.co.uk] * NOPI [https://bookshop.org/p/books/nopi-the-cookbook-yotam-ottolenghi/12837615] * Octomore [https://www.bruichladdich.com/collections/octomore]

Ranjit Jhala

In the inaugural episode of Current Continuation, we talk to Prof. Ranjit Jhala [https://ranjitjhala.github.io/] 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 [https://blog.sigplan.org] * Sinclair Spectrum [https://en.wikipedia.org/wiki/ZX_Spectrum] * Ben Liblit [https://pages.cs.wisc.edu/~liblit/] * Thomas Henzinger [https://pub.ista.ac.at/~tah/] * George Necula [https://people.eecs.berkeley.edu/~necula/] * Alex Aiken [https://theory.stanford.edu/~aiken/] * Rupak Majumdar [https://people.mpi-sws.org/~rupak/] * 2009 software model checking survey by Ranjit and Rupak [https://dl.acm.org/doi/10.1145/1592434.1592438] * SPIN [https://spinroot.com/spin/whatispin.html] * VeriSoft [https://9p.io/who/god/verisoft/] * SLAM [https://www.microsoft.com/en-us/research/project/slam/] * Joseph Goguen [https://cseweb.ucsd.edu/~goguen/] * “Lazy Abstraction,” POPL 2002 [https://dl.acm.org/doi/10.1145/503272.503279] * Sriram Rajamani [https://www.microsoft.com/en-us/research/people/sriram/] * “Liquid Types,” PLDI 2008 [https://dl.acm.org/doi/10.1145/1375581.1375602] * Hongwei Xi [https://www.bu.edu/cs/profiles/hongwei-xi/] * Frank Pfenning [https://www.cs.cmu.edu/~fp/] * Dependent ML [https://en.wikipedia.org/wiki/Dependent_ML] * Rust [https://www.rust-lang.org] * Lean [https://lean-lang.org] * Greg Morrisett [https://www.cs.cornell.edu/~jgm/] * Mike Dodds [https://galois.com/team/mike-dodds/] * “N things I learned trying to do formal methods in industry,” a talk by Mike Dodds [https://youtu.be/gfvvowAc130] * “Flux: Liquid Types for Rust,” PLDI 2023 [https://dl.acm.org/doi/10.1145/3591283] * Flux on GitHub [https://github.com/flux-rs/flux] * Simon Peyton Jones [https://simon.peytonjones.org] * Verse [https://dev.epicgames.com/documentation/en-us/uefn/verse-language-reference] * “The Verse Calculus: a Core Calculus for Functional Logic Programming,” ICFP 2023 [https://dl.acm.org/doi/10.1145/3607845] * Tim Sweeney [https://en.wikipedia.org/wiki/Tim_Sweeney] * Jan Vitek [https://janvitek.org] * Sam Tobin-Hochstadt [https://samth.github.io] * David Van Horn [https://www.cs.umd.edu/~dvanhorn/] * “Higher-Order Symbolic Execution for Contract Verification and Refutation,” JFP 2016 [https://www.cambridge.org/core/journals/journal-of-functional-programming/article/higher-order-symbolic-execution-for-contract-verification-and-refutation/129E10B4113242ABB0B7D6890CCFDBC9] * Liquid Haskell [https://ucsd-progsys.github.io/liquidhaskell/] * Concrete Semantics [http://www.concrete-semantics.org] * Isabelle [https://isabelle.in.tum.de] * Software Foundations [https://softwarefoundations.cis.upenn.edu] * Virginia Vassilevska Williams [https://people.csail.mit.edu/virgi/] * Halide [https://halide-lang.org] * “How to Design Talks” [https://youtu.be/QFNYdJmUH_w] * “How to Design Programs” [https://htdp.org]