Jeremy @jeremysiek@types.pl

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

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!

https://pigeonholed.co/starting-bayrise

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?

FAILURE TO OPTIMIZE:
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

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 :-)

https://leanprover.github.io/functional_programming_in_lean/

Racket is now on mastodon!

Gradual Typing for Effect Handlers

Max S. New, Eric Giovannini, Daniel R. Licata
https://arXiv.org/abs/2304.02145 https://arXiv.org/pdf/2304.02145

tail calls shipping in v8! (but just in webassembly :) https://v8.dev/blog/wasm-tail-call

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! https://scientistseessquirrel.wordpress.com/writing-resources/

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

https://djvelleman.github.io/HTPIwL/

"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!

PLDI SRC submission deadline is in 2 days! https://pldi23.sigplan.org/track/pldi-2023-src

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

This year's PLDI is also part of FCRC (https://fcrc.acm.org/) which contains many different and interesting CS conferences.

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

I'm presenting

"A Caret for Your Thoughts: Adapting Caret (Ꮖ) Navigation to Visual Editors"

at PX/23 in 10 hours!

https://2023.programming-conference.org/details/px-2023-papers/1/A-Caret-for-Your-Thoughts-Adapting-Caret-Navigation-to-Visual-Editors