Revisiting CS101.

Had a fantastic week teaching Programming with Proofs in Lean at Neapolis University Pafos. It was great to introduce NUP students to program verification with Veil and Velvet, having many insightful discussions along the way. Excited to see what projects they'll develop next!

We are hiring! Suzanne Embury and I are looking for a talented Ph.D. student 👩‍🎓👨‍🎓 to join an exciting, high-impact project on automated testing and bug fixing of Formal Methods tools. www.findaphd.com/phds/project...

Spent the last couple of days porting my program verification class from Dafny to Lean via Loom/Velvet, and it just works! Whenever the SMT solver can’t fully prove a program correct, Lean’s aesop and grind take care of the remaining goals.

Grokipedia is alright.

A reminder that we will have another @icfp-conference.bsky.social/SPLASH nature walk planned for tomorrow. Consider joining if you are (still) in Singapore! 2025.splashcon.org/attending/ou...

The tunes of Rocq’n’Roll. #icfpsplash25

FARM Performance is about to start! #icfpsplash25

Lots of folks in the OxCaml tutorial! #icfpsplash25

@icfp-conference.bsky.social Had a nice day co-hosting the first hike of #icfpsplash25 Outdoor Activities track with Yibo🙌 Walking in the forest 🌳 Seeking special animals (monkeys🐒, lizards🦎, colugos🦇, and even a snake🐍!) Enjoying the networking🥳

It seems the first hike as part of @icfp-conference.bsky.social/SPLASH went well! A shoutout to @ningkeli.bsky.social and Yibo DONG (as well as my wife, Ting), who guided the participants on this walk. I could unfortunately not participate, as I had to travel abroad due to an urgent issue.

1st coffee break of the week many many more to come #icfpsplash25

ICFP/SPLASH is starting now!! See you all at NUS today — #icfpsplash25

The UBC Software Practices Lab is heading to #icfpsplash25! 4 ICFP/OOPSLA talks, 1 SPLASH-E, 5 talks at associated workshops... check it out: www.cs.ubc.ca/news/2025/10...

A beautiful day to stop in at the Singapore Botanic Gardens and the National Orchid Garden before ICFP/SPLASH! #icfpsplash25

ICFP/SPLASH'25 is starting tomorrow! Attending Sunday workshops and FARM Performance at #icfpsplash25? Make sure check out our illustrated guide on getting to NUS Conservatory and dining options on campus: conf.researchr.org/venue/icfp-s...

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-...

One week until ICFP/SPLASH’25! conf.researchr.org/home/icfp-sp...

@mathieu.social will be presenting a functional pearl "Invertible Syntax without the Tuples", joint work with Arnaud Spiwack, at Olivier Danvy's Festschrift on the Tuesday 14th. conf.researchr.org/details/icfp...

And if you’re interested in OxCaml, we have a tutorial on Sunday at ICFP walking through it conf.researchr.org/track/icfp-s... (materials will be online for anyone afterwards. Just the minor detail of finishing writing them first)

An opening theme from the Outlaw Star series has just randomly started playing in my head, and now I am fighting the urge to rewatch it.

I’m looking for an intern to work on Rust/RustRover content creation. If you are a university student in any EU country, the UK, Serbia, or Armenia, and you are passionate about Rust and sharing your knowledge, I’d love to hear from you. Please repost to help spread the word. Links below.

T minus 3 weeks!! I wonder how many ICFP 2025 papers I can read on the plane ride over?

Now that the competition is over, Adso has penned his reflections. icfpcontest2025.github.io/afterword.pdf We also have many team write-ups here: icfpcontest2025.github.io/writeups.html Please let us know if you have some to add to the list!

Just visited YST Conservatory of NUS, the venue for the upcoming FARM concert at ICFP/SPLASH'25. Excited about the upcoming performance combining art, music, and creative programming! 2025.splashcon.org/track/splash...

OlivierFest’25 is taking place on October 14-15 at ICFP/SPLASH'25 in Singapore! A two-day celebration of Olivier Danvy's impact on PL research, with a program packed with talks on algebraic effects, semantics, interpreters, and, of course, continuations. conf.researchr.org/home/icfp-sp...

It's official: RTFM, the faculty mentoring workshop, is happening again, this time at POPL 2026 in Rennes. The one we had at PLDI 2024 in Copenhagen was well received, so I'm looking forward to the next edition. Stay tuned!

"Pat, why do you carry that ridiculous 600mm lens on long hikes?" Buddy, I can see mountains reflected in the eyes of a trailside pika.

I will be organizing two nature walks for ICFP/SPLASH (‪@icfp-conference.bsky.social‬)! I did one of them this weekend and was very lucky to see 11 saltwater crocodiles (including a tiny baby one), countless monitor lizards, otters, macaques, fruit bats, various kinds of birds, and fish.

ICFP/SPLASH goers -- looking to escape into the wild for a moment? Come join one of these two planned hikes (courtesy of @mrigger.bsky.social)! First through the central reserve, and second through the wetlands: 2025.splashcon.org/attending/ou...

Already registered for SPLASH or @icfp-conference.bsky.social? If not, check out our list of accepted papers: conf.researchr.org/home/icfp-sp... It's language implementation techniques, from debugging and JIT compiling on microcontrollers to visualizing execution patterns between CPU and GPU!

Do it for science!

ICFP/SPLASH attendees: what's the first thing you're doing in Singapore this October?? my goal: try every single dish on this list 👀 👀 conf.researchr.org/attending/ic... (courtesy of @ilyasergey.bsky.social !)

It was a pleasure to host @kcsrk.info who visited NUS earlier this week and talked about some cool systems verification projects done by his team.

ICFP/SPLASH 2025 registration is open! If you register soon, you can catch the early registration discount (by August 31). Register for the whole 7 days and only pay for 6! conf.researchr.org/attending/ic...

Moshe Vardi is Simon Peyton Jones of CAV.

The call for nominations for SIGPLAN Research Highlights for 2024 is open! Deadline: 15 August 2025. Nominate your favourite paper from the last year's POPL, PLDI, ICFP, OOPSLA, PPoPP, and ASPLOS via this form: forms.gle/mE3Qf2AJfSTN...

Fun fact: if you write a paper on Separation Logic in Cursor with AI suggestions on, it start suggesting text citing papers by @herrdreyer.bsky.social.

It was a great pleasure to host Sebastian Ullrich from Lean FRO at NUS and learn about Lean 4 roadmap and its upcoming module system.

the ICFP 2025 program is coming together! Check out our list of accepted papers: icfp25.sigplan.org/track/icfp-2... and we'll have three keynotes this year! icfp25.sigplan.org/track/icfp-2... ⬇️⬇️⬇️

I really like my job.

In Seoul this week. Just got this delicious local treat from a street vendor.

The 2025 Managed Programming Languages & Runtimes Conference (MPLR) CFP is out and extended - June 24! Regardless of which managed language you use, if you come from industry or academia, or if you develop tools or compiler optimizations, MPLR has a track for you! conf.researchr.org/home/icfp-sp...

One of the cutest small traditions we have in my research lab is, when travelling, to put a flag of the current location into the Mattermost status.

MPLR extended its deadline to June 24th to better align with some other notification dates. Two more weeks to submit your work on language implementations, VMs, compilers, interpreters, and tooling! conf.researchr.org/home/icfp-sp...

PLMW is calling for student applications -- if you are a student interested in ICFP/SPLASH 2025, consider applying! Deadline: July 15, AoE conf.researchr.org/home/icfp-sp...

One month till POPL deadline.

The fact that someone made a one hour video about the flight I take every couple of years and it has been watched 90k times is, probably, a sign that my life is a lot more interesting than I think. (Also, feeling like a jaded survivor in my regular economy class.)

Did some vibe proving today.