I'll be at ICFP/SPLASH in Singapore, starting in a little over a week! Really looking forward to seeing everyone.
Harry Goldstein
@harrisongoldste.in
(he/him) Postdoc at the University of Maryland I make tools that help developers to build trust in their software using techniques from PL, SE, and HCI. Currently on the academic job market, looking for tenure-track positions! https://harrisongoldste.in
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/
Think Globally, Discuss PL Locally
In-person meetings are hugely beneficial for academic research; they provide a venue to collaborate and connect, making our community more connected and facilitating the exchange of ideas. In addit…
blog.sigplan.org
Upstate 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.
Upstate PL August 2025
cs.cornell.edu
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
If one of the greatest math minds of our generation accepts incorrect AI generated code as correct, you will too youtube.com/clip/Ugkx0fA...
YouTube
Share your videos with friends, family, and the world
youtube.com
I'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 still have my Twitter account because I want to make sure folks can reach me for job market reasons, but I *cannot* wait to delete that account. The last few times I've logged in to check notifications I've seen videos of people getting injured on the main landing page? I don't need this
I feel a little bad about this, but at this point I think the only way to get remotely useful customer service from Xfinity (and maybe others) is to ask the AI bot to cancel your account. Within seconds it gives you a phone number for a human, and then those folks are usually very helpful!
I’m going to be at POPL next week, but only for two days (Wednesday and Thursday)! If you want to make sure we get a chance to chat, ping me here or via email so we can plan a time
Penn’s annual PL REU is accepting applications for Summer 2025! penn-repl.github.io REPL is an awesome program. It’s fully funded (housing / travel / stipend) and you get to do research with an amazing group of people Deadline is March 15th—if you’re an undergrad that likes PL, you should apply!
REPL
penn-repl.github.io
Thanks so much to JFP for publishing my dissertation abstract, along with 9 others! This is a really valuable service for the community. Dissertations are a ton of work, and it’s nice to have a way to increase the chance that they’ll be read and used
We're delighted to publish ten PhD abstracts in this round. Topics range from types to tests, from synthesis to software engineering, from datatypes to differentiation. Have a look!
Does anyone have advice around putting ongoing work in job talks? I have some exciting stuff in the pipeline that I'd love to share with folks, but it seems hard to do that without poisoning potential reviewers
Can someone do a psychological study on what Rocq/Lean proofs do to users' brains? I've been doing some Lean proofs lately, and it focuses my attention in a way that almost nothing else does. And if I try to pull myself away in the middle, I find it very hard to context-switch
I know I already posted about Lean once today, but I had to share: apparently new Lean projects automatically have CI set up?? github.com/leanprover/l... Amazing. I know it isn't hard to set up yourself, but I almost never use CI on personal projects because it's just a little too much of a hassle
GitHub - leanprover/lean-action: GitHub action for standard CI in Lean projects
GitHub action for standard CI in Lean projects. Contribute to leanprover/lean-action development by creating an account on GitHub.
github.com
Folks may have already seen on the bird site, but I was on the Haskell Interlude! t.co/uyilDdNV9T It was a ton of fun! If folks want to know more about anything we talked about let me know
https://haskell.foundation/podcast/59/
t.co
Here's another short from my conversation on TheForkJoin! https://youtube.com/shorts/n69-xVE5Pqg?feature=share
You guys are getting paid? #phd #academia
This is a clip from when I was a guest on TheForkJoin with Rachit Nigam and Oliver Flatt (twitch.tv/TheForkJoin or youtube.com/@theforkjoin)
youtube.com
Experimenting with short-form video, so I made a little follow up to my conversation last week on http://twitch.tv/theforkjoin. Stay tuned, I may post a few more clips from the conversation! https://youtube.com/shorts/2oDq31vzCkA
What does "PhD candidate" mean? #academia #phd
This is based on a podchat I did with the TheForkJoin! Check them out at twitch.tv/theforkjoin
youtube.com