Junrui Liu

Interactive Theorem Provers for Proof Education | Proceedings of the 2025 ACM SIGPLAN International Symposium on SPLASH-E

Interactive theorem provers for proof education. ~ Romina Mahinpei, Manoel Horta Ribeiro, Mae Milano. dl.acm.org/doi/abs/10.1... #ITP #CoqProver #Teaching

Write your own tiny programming system(s)! - YouTube The goal of this course is to teach how fundamental programming language techniques, algorithms and systems work by writing their miniature versions. The cou...

I'm teaching 𝗪𝗿𝗶𝘁𝗲 𝘆𝗼𝘂𝗿 𝗼𝘄𝗻 𝘁𝗶𝗻𝘆 𝗽𝗿𝗼𝗴𝗿𝗮𝗺𝗺𝗶𝗻𝗴 𝘀𝘆𝘀𝘁𝗲𝗺(𝘀)! again. I'll be posting the videos & tasks on YouTube too.

In the first lecture, I explain what's a tiny system, why write one and show plenty of demos!

🎞️ Playlist: www.youtube.com/playlist?lis...
👉 More info: d3s.mff.cuni.cz/teaching/npr...

Sorry, I meant alternative instead of selective. Time to go back to OCaml…

I had a random thought (when reading the free generator paper) that the selective applicative interface with a ”f a * f b -> f (a*b)” API instead of the usual “<*>” roughly corresponds to typed context-free expressions minus fixpoint. Might explain the expressiveness vs understandability tradeoff…

A Data-Centric Introduction to Computing This book is an introduction to computer science. It will teach you to program, and do so in ways that are of practical value and importance. However, it will also go beyond programming to computer sc...

Super excited to release the latest version of "A Data-Centric Introduction to Computing" (DCIC). See release notes for 2025-08-27 for what's changed and new (a LOT!): dcic-world.org/2025-08-27/R....
dcic-world.org

The most enlightening explanation on subtyping I read was from Benjamin Pierce's PhD thesis. Paraphrased, subtyping is type-directed program synthesis (intersection types synthesize tuple projections, nat<int synthesizes coercions, function contra & covariance synthesize function composition)

YouTube video by Jonathan Aldrich PLP 1.3-1.4: Compilation, interpretation, and environments

Released today: the second video in my Programming Language Pragmatics series, covering Compilation, Interpretation, and Environments!

www.youtube.com/watch?v=mrmo...

Going forward, I'll post a video 3 times a week. Please share the series with anyone who might benefit!

wow this sounds super interesting. Looking forward to reading your paper when it comes out!

YouTube video by Kristopher Micinski Minnowbrook Logic Programming Seminar (Supercut w/ Extras)

May 25-27, 2025, I hosted an event, the "Minnowbrook Logic Programming Seminar," in Blue Mountain Lake, NY. I recorded 11 talks on Datalog-related interests, totaling over 9+ hours of video, which I have just now published on YouTube youtu.be/3ec9VfMUVa8

The joy of comp sci is that it applies scientific (mathematical, if you're lucky) thinking to a domain which is constructed entirely artificially. Things are the way we make them. Reality doesn't fling you around: you fling reality around. And you need to learn to do so with skill and consideration.

Specifically, if you're looking for a CS job at a small liberal arts college check this list (later this summer): cs-pui.github.io

And warning: many of these jobs have early fall deadlines!

#FAccT2025

And here's a blog post, announcing the release!

blog.janestreet.com/introducing-...

was even thinking about designing an automata theory course around this idea: regex is just like a simple imperative language with atomic print(), but with if's and while's conditions being non-deterministic. Then everything becomes "predicting what a program will print by abstracting it into regex"

This is such an important observation that I've been planning to delve into it in my intro PL class this summer. In this sense, non-determinism is just like type abstraction: if an over-approximation of actual behaviors is proven safe, then so are the actual behaviors.

U.S. Will ‘Aggressively’ Revoke Visas of Many Chinese Students, Rubio Says

Breaking News: The U.S. government will work to “aggressively revoke” visas of Chinese students, Secretary of State Marco Rubio said.

UPDATE: I am going to offer some free online training this summer about how to create code playbacks and use them in a course. I'll show how I use code playbacks instead of textbooks and videos and share what my students think of them.

www.eventbrite.com/e/beyond-tex...

A few thoughts on AI and education, from someone who uses AI and also teaches many levels of student.

1. Most importantly, it's not possible to know what will happen because no one knows what skills AI will or will not replace in the next few years.

Thanks for your fast response! I'll shoot an email

Hi Prof. Friedler, I'm very interested in applying for this position, and have some questions about the application materials for which I'd really appreciate your input! However, Bluesky doesn't seem to allow me to DM you via its Chat. Would you prefer me to reach out via other channels instead?

Really excited to teach an undergrad course on programming languages this summer! Unfortunately, UCSB only gave me 6 weeks for a summer class, so will have to work under severe time constraints. Slowly working out the course design here (suggestions welcome!): junrui-liu.github.io/cs162/

haven't implemented a server myself, but some examples on my mind: syntax highlighting (parsing), debugger (small-step operational semantics), autocompletion suggestion (type checking for pruning), typed holes (bidirectional typing a la Hazel/unification-based inference)

Random thought: teaching a PL course where students progressively build components of a language server for a simple language

This essay about feminism in PL asks some really tough questions!

It’s making me wonder: what should the purpose of PL research be, anyway?? Are we trying to “solve problems”, “make the world a better place”, “expand knowledge”, or…?

www.felienne.com/wp-content/u...

On a possibly related note, Dolan's paper also cites Graphs, Dioids and Semirings (Gondran & Minoux), which describes the generalized Dijkstra algorithm on semirings (p.144)

quick update: the "paper" I was thinking about but whose title I couldn't recall was this one: youtu.be/TQUvXy547AA?...

yeah no prob! I'm been thinking about something slightly related to this, so if you found anything interesting please lmk

This paper (yzsun.me/files/TFP22-...) might be tangentially relevant but it just encodes labelled arguments as records. IIRC there was another recent paper at one of the PL conferences (POPL/PLDI/OOPSLA?) that had a core calculus purely based on labels but I can't recall the name of the paper.

I tried sneaking Church encodings into a PL class as extra credit when i was a TA & found Parigot encodings easier to teach: nats = their induction principle, sub1 is free, and it's a straightforward syntax-directed translation from the original recursive definitions of + * ^ to their encodings