Jeremy boosted

The recording of the POPL 2023 talk “An Order-Theoretic Analysis of Universe Polymorphism” is already on YouTube! 🤩
Joint work with Carlo Angiuli and @totbwf

Jeremy boosted

Unapologetically boosting this because it's a nice story about a kid who fell in love with computing through @PyretLang (which runs fine on 6yo computers) and now runs his own education program. Go Isaac!

PLDI/FCRC Tutorial: Teaching and Learning Compilers Incrementally
Saturday June 17, 2pm to 6pm, in Orlando Florida
Register this week for early bird pricing!

Jeremy boosted

As per tradition, the last question of my compilers final was:
Write a haiku about compilers. 0.5 points if funny, 0.5 points if actually a haiku. These are some of the best ones (some are not haikus):

Terminate your string
If you do not I will scream
Sincerely, scanner

Compilers be cool
Cool as a cucumber, ya?
Nah, it got that rizz!

If not type checking
One plus true will make you blue
Typechecking saves you

Lex and parse the code
Oops, I forgot to typecheck
What is true times 2?

Poorly written code
My compiler does nothing
Poorly written MIPS

Dearest Professor
With beautiful golden hair
Teach us compilers

push push pop pop push
Wait, what was I doing again?
push push pop pop push

Wow, my code is slow
I tell GCC, “-o3”
Not my problem now

Compile fast don’t blink
Errors all over the place
French programmers stink
Note: I think this was related to me making fun of whoever named Coq

Linguist in compisci
Switch majors free of Chomsky
Wait, ho’d he get here?

I make compilers
I grow (abstract syntax) trees
I’m a gardener

Find the access link
Follow where the link points to
Make a smile and blink

From spaghetti code
To an abstract syntax tree
To lasagna code

I: don’t write poems
But I wrote a compiler
j I # Ha Ha Ha

Yahoo! Finished a proof of the gradual guarantee for the gradually-typed lambda calculus in Agda using step-indexed logical relations:

Now I need to reflect on what I learned from the ordeal! And there's plenty of polishing/simplifying to do.

Jeremy boosted

The final prerelease of Functional Programming in Lean is out! If you have time, I'd really appreciate any feedback you can provide on the final chapter before my deadline at the end of the month. But even more, I hope that you find it valuable and enjoyable :-)

New blog post: Type Safety in 10 Easy, 4 Medium, and 1 Hard Lemma using Step-indexed Logical Relations (in Agda)

Jeremy boosted
Jeremy boosted
Jeremy boosted

Super excited to finish another mechanized proof of type safety! 😂 This time using logical relations and a logic for step indexing that I built in Agda with some help from Phil Wadler and Peter Thiemann.

Jeremy boosted

Just your occasional reminder that I kep a curated list of resources for scientific writing - books, web sites, apps, webinars, etc. There's probably something here to help with almost any writing issue! scientistseessquirrel.wordpres

Jeremy boosted

Daniel J. Velleman has translated parts of his classic text "How to prove it" into Lean 4!

"How to prove it in Lean" goes through examples in the original book, and discusses how they can be proved in Lean. He also talks about how Lean's use of type theory rather than set theory affects this kind of basic mathematics, and furthermore gives clear installation instructions for anyone who wants to play along at home!

Jeremy boosted

PLDI SRC submission deadline is in 2 days!

PLDI SRC has a two-track model that supports both in-person and remote presentations.

This year's PLDI is also part of FCRC ( which contains many different and interesting CS conferences.

Jeremy boosted

A student just told me that my FP class was the best class they took this term. That made my day! 💃

Compiler tidbit: a tail call is a call immediately followed by a return. A compiler can save space by emitting instructions to pop the current frame before making the tail call. An upshot of this optimization is that tail recursive procedures use constant stack space.

Jeremy boosted

Compiler tidbit: computing which variables are live at an instruction depends on which are live in the following instruction. But what if there are cycles in the control flow? Start with no live variables at every instruction and recompute until the answer stops changing.

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.