A problem that COVID and LLM subscription services share is that the “let ‘er rip” and “maximum caution” stances are more or less well defined but if two people say they’re being cautious about exposure you can be almost sure one of them is still doing stuff that absolutely horrifies the other.
Pleased to announce shplait/liquid, a liquid-typed version of shplait, the language of my book PLAI. This version adds liquid-typing, a form of refinement types. It's primarily meant to be a small language for pedagogic purposes to induce people to try grown-up ones later. ↵
Too many people are calling on the community to "change how we value papers".
Not enough people are posting "this is what we look for in our next hiring round".
Do not "use LLMs for the boring bits". Use what boring about the boring bits for the boring bits. If you can't, either those bits aren't boring, or you're using the wrong tools.
There is, remarkably, basically no good FOSS software for the task of syncing slides (in the form of PNGs) to audio. I’ve tried a bunch and they’re all deeply broken. If anyone has suggestions, I’m all ears
[Reposting—Also, extended talk submission deadline!]
The 2026 Midwest PL summit will be on November 6th in Iowa City. This is an informal workshop, intended to spread ideas and foster collaboration among the (Greater) Midwest PL community. Registration is free, and student travel grants are supported by NSF.
Please register talk or poster abstracts by October 12th, and register to attend by October 26th. For registration forms or more details, check out https://2026.mwpls.org.
If you teach deduction as a system to be studied, rather than a skill to be acquired, you do your students a disservice.
who's at OOPSLA that I should talk to while y'all're here?
(equivalently: who at OOPSLA wants to talk to me while y'all're here?)
A message from my colleague Benedikt Ahrens:
Hi all,
I have funding for a postdoc position at TU Delft on combining computer proof assistants and computer algebra systems in the area of category theory, and I would be happy to hear from potential applicants before the formal advert goes out.
I am looking for someone who is interested in all three of proof assistants, computer algebra systems, and category theory, and who has some experience in at least one or two of them.
The position ideally starts no later than March 2027.
If you are interested, please email me at B.P.Ahrens@tudelft.nl with a short note about your background and your research interests. Informal questions are very welcome.
Please feel free to forward this to anyone who might be a good fit.
Best wishes, Benedikt
Update: the position is now open!
So aufgeregt auf morgen: zum ersten mal unsere mobile Mosterei ausprobieren https://youtu.be/dT2L_SqJBYA?si=6H-sOjk66Y-ASXu7
Die letzten Tage schonmal Äpfel gesammelt - 2 Hänger sind voll, und noch ein paar Kisten und ein big bag...
Falls in den nächsten Monaten wer Apfelsaft mag, sagt Bescheid. Gibt es gegen Spende an Barnim für alle (Empfehlung 15€ für den 5l bag in a box).
Um, did someone accidentally delete POPL?
I'm going to be at RacketCon on Saturday and SPLASH from Sunday to Thursday. I'll be giving a keynote at SPLASH-E ("Teaching About Tools For Thought"), a talk at PLMW ("The Art and Science of Teaching Rust"), and I'm co-organizing HATRA... all on Sunday!
I want to see all my wonderful PL colleagues, so please find me in the hallways or email me at will_crichton@brown.edu if you want to get coffee / dinner / etc.
Also: I am recruiting PhD students for next year. If you're interested in my lab, let's chat! See my website (https://willcrichton.net/) for more specific topics I've been thinking about.
I've started my new job! As of today, I'm a postdoc in the Software Science group of the Institute of Computing and Information Sciences at Radboud University in the Netherlands.
This position is (largely) funded by a personal 3-year Veni fellowship from the Dutch research organization NWO.
I'm very happy about this and I wanted to use this occasion to write a somewhat personal thread with some acknowledgements.
[1/3]
The New Jersey Programming Languages and Systems Seminar's (NJPLS) date has been set for November 13th at Jane Street's office in Manhattan! Registration is free as usual and talk proposals are open until October 20th! Please consider signing up if you feel like making the trip and if possible propose a talk, it's a very nice community and all talks related to PL or PL-y systems are welcome! As usual the notion of "new jersey" is a vibe more than a specific place, all are welcome!
For my birthday, my brother-in-law gave me a 4992-digit hex number that, when used as a seed for Python’s random number generator, makes it so that printing a sequence of “random” ASCII characters actually prints a birthday greeting.
I find it rather amazing that this is possible!
This is the program he sent with the seed:
with open("seed.txt", encoding="ascii") as handle:
seed = int(handle.read().strip(), 0)
r = random.Random(seed)
pending = ""
while True:
character = chr(r.randrange(128))
if pending + character == "\x1e\x1f":
break
print(pending, end="")
pending = character
print()
I don't have a lot of reach on here, so boosts would be greatly appreciated.
I'm looking for someone to join my team at the Lean FRO as a metaprogrammer with a view towards library quality.
I'm working toward a future in which ITPs are a joy to use productively for mathematics and software verification. I believe that to get there, we need to get a lot better at building libraries that are complete, consistent and scalable, and a key factor in that will be to have excellent tooling for monitoring and improving the quality of our libraries.
At the Lean FRO, we are building such tools. This includes our linting framework and many elaborator features, but it also extends to more advanced tools, such as our work-in-progress library QA management tool Grove, which I talked about at EuroProofNet last year. And we have many more ideas (and you might as well!).
If you are interested in helping make Lean a better tool for building high-quality proof developments, please message me! Ideally, you have experience with Lean metaprogramming or building other PL-related tooling, and/or have thought a lot about how to build high-quality proof libraries in an ITP (doesn't have to be Lean).
This is a fully remote, full-time or part-time position. The Lean FRO is able to hire people from most places in the world.
Link to my (slightly outdated) EuroProofNet talk: https://youtu.be/qb9kN6ligY4
Congratulations! We are pleased to let you know that your paper “Commuting Conversions and Join Points for Call-By-Push-Value” has been selected to receive an OOPSLA 2026 Distinguished Paper Award.
are you sure?????
I’m delighted that a paper I co-authored with my brilliant colleague, Franz Berto, on some connections between logic and the psychology of reasoning, has been accepted for publication in the Review of Philosophy and Psychology.
We sketch some possible connections between System 1 and System 2 thinking and different accounts of the semantics of negation.
A preprint is now available here: https://consequently.org/writing/rwn/
How we learned to stop worrying and love campus surveillance cameras (with AI!).
https://fnl.mit.edu/how-we-learned-to-stop-worrying-and-love-campus-surveillance/