@ngernest2.bsky.social
PL/Systems PhD student at Cornell ngernest.github.io
I am thrilled to announce Velvet: a new foundational multi-modal verifier for imperative programs in Lean.
Velvet unifies execution, testing, automated and interactive proofs; and is itself proven sound.
π» github.com/verse-lab/loom
π verse-lab.github.io/papers/loom-...
Have you been considering hosting a local PL meetup? Need a good place to start? Check out the PL Perspectives post that I wrote with Michael Greenberg and Noam Zilberstein!
blog.sigplan.org/2025/09/16/think-globally-discuss-pl-locally/
Last week, we were treated to an extraordinary talk internally at @oxide.computer. It was at once an expository talk of a complicated software system and an experience talk of developing systems software in the large -- and it was far too good to keep to ourselves! oxide.computer/blog/systems...
18.09.2025 17:29 β π 94 π 18 π¬ 3 π 7
This was a great talk from Will Crichton. I think Will's approach to approaching questions around language tooling and teaching is compelling, though I wonder how far the approach can scale!
youtu.be/R0dP-QR5wQo?...
type hierarchy with universes Eq.rfl 2 is of type 2 = 2, which itself is of type Prop, which itself is of type Type, which itself is of type Type 1, which itself is of type Type 2, and so on. also we have for example numbers 0 1 2 which are of type Nat, which is of type Type, and so on. also we have stuff like Set of Type, which is of type Type 1. or Set of Type 1, which is of Type 2. you get the idea
doodling: lean type hierarchy
15.08.2025 00:46 β π 63 π 5 π¬ 5 π 1Choreographic Ξ»-calculi are a hot topic. You might know models like Pirouette (POPL 2022) or ChorΞ» (ICTAC 2022).
But did you know researchers don't agree what the "right" semantics should even be?
Our ICFP pearl builds a tiny calculus from scratch, and shows the right semantics is... non-strict!?
Summer Undergraduate Internship - reposts welcome!
Are you a senior undergrad, interested in Programming Languages? Do you want to visit Canada for a paid 12-week internship?
Right this is how Iβm going to do our ICFP talk @patrick.sirref.org! Very cool to see OCaml web components to make executable notebooks online really easy patrick.sirref.org/slipshow-x-x...
23.07.2025 17:59 β π 10 π 4 π¬ 1 π 0Upstate NY folks: Cornell will be hosting Upstate PL (www.cs.cornell.edu/upstate-pl/) on Thursday, August 28th. You should come if you're in the area!
Talk proposals are due August 4th, registration closes August 18th.
Really enjoyed this talk by @harrisongoldste.in that demonstrates inventive uses of the #LeanLang InfoView enhanced by metaprogramming techniques to display real-time testing data.
#LeanProver #Metaprogramming #VSCode #PropertyTesting
Some more exciting news! This year we had not one, but two(!) dissertations receiving the SIGPLAN John C. Reynolds Doctoral Dissertation Award at PLDI!
The awardees are: Harrison Goldstein from the University of Pennsylvania and Rachit Nigam from Cornell University. More info β¬οΈ
Nice post on costs and benefits of formal methods, by @m-dodds.bsky.social: www.galois.com/articles/wha...
25.06.2025 21:01 β π 26 π 4 π¬ 0 π 0You can try Janestreet's #OCaml with modes in your browser at patrick.sirref.org/oxcaml
09.05.2025 13:58 β π 9 π 5 π¬ 2 π 0
If you are considering applying for a PhD this Fall, please get in touch. Iβm looking for students who are interested in PL, SE, and/or HCI β and ideally all three! You can find more information about me and my work on my website: harrisongoldste.in
07.05.2025 18:38 β π 18 π 11 π¬ 2 π 1I'm incredibly excited to announce that I've accepted a tenure-track position as an assistant professor at the University at Buffalo!
The PL/SE group at UB is already really impressive, and I am honored to be part of its continued growth
I wrote up a quick post about the OCaml to Hazel transpiler I've been hacking on recently. Reusing OCaml's type inference to handle Hazel's explicit polymorphism has been pretty fun!
patrick.sirref.org/hazel-of-ocaml
Next week at ESOP 2025 (European Symposium on Programming) in Hamilton, ON (not in Europe) I'll be giving a talk on Stratified Type Theory! (Tue 6 May 10:30 am)
We replace stratified type universes with stratified judgements, and restrict dependent function domains to strictly smaller levels.
new book on session types just dropped!
www.cambridge.org/us/universit...
In 2023 I curated a 100 year timeline about hardware implementations of functional programming languages. Best viewed on a desktop or laptop screen. I occasionally add to it.
haflang.github.io/history.html
slides for my talk at #EpicWebConf2025
docs.google.com/presentation...
Just skimmed through the paper, such a cool idea! I would love to be able to use Allegro as a drop-in replacement for Base_quickcheck for my future OCaml testing needs
26.03.2025 03:23 β π 3 π 0 π¬ 0 π 0
Calling for Presentations!
Higher-order, Typed, Inferred, Strict:
The 2025 ML Family Workshop welcomes presentations on any topic related to programming languages in the ML family (such as SML, OCaml, F#, etc.)
Submissions due: June 19 AoE
Workshop: Oct 16
conf.researchr.org/home/icfp-sp...
Great work from @tarides.com folks on pragmatic verification of OCaml software.
Chosen as one of the distinguished papers at TACAS 2025.
Paper: janmidtgaard.dk/papers/Huber...
Code: discuss.ocaml.org/t/ann-ortac-...
An excellent first introduction to logical relations:
arxiv.org/abs/2309.15724
I'm writing a new blog series on practical implementation of substructural type systems, in Idris!
The first blog post will look at substructural polymorphism and why it's *hard*, harder than people assume on first glance!
zanzix.github.io/posts/5-subs...
