Anyway, all of these ideas are too cool to pass up. Iโll definitely try combining this with the "compilers-as-fixed-points" approach next time I get to teach the course!
Alas, a quick search revealed Ras had taught this for years in his once-famous "Hack Your Language" course. I think the notes are based on the paper Parsing and Generation as Datalog Queries by Kanazawa. He shows how semi-naive = CYK and magic-set = Earley.
homes.cs.washington.edu/~bodik/ucb/c...
Then it clicked: Datalog is essentially "fancy" graph transitive closure! Their algorithm can be recast as the evaluation of a Datalog program, where the input string forms the EDB and the grammar induces the IDB. Parsing effectively becomes solving Datalog.
This was eye-opening, but I felt parsing was the missing piece. Could bottom-up parsing also be phrased this way? Later, I found inspiration in this paper by Esparza et al.: arxiv.org/pdf/2410.19386. They view parsing as the transitive closure of a graph constructed from the input string.
A while ago, I came across Neel Krishnaswami's bold idea of centering an intro compilers course on the bottom-up evaluation of least fixed-points. Since so many compiler passes and static analyses can be framed this way, itโs a powerful unifying theme.
semantic-domain.blogspot.com/2020/02/thou...
New on my blog: "Why Study CS? Thoughts on LLM-assisted software engineering" kmicinski.com/claude-code-...
Over the years I've been asked many times for advice on pedagogy, what to read to learn more, etc. I've finally put together a bunch of materials into one blog post: Key Advice โข Readings โข Neuromyths โข For Computer Scientists โข Classroom Tips. Enjoy!
parentheticallyspeaking.org/articles/ped...
Added to my holiday reading list. Looking forward!
A more update-to-date text using the same approach: link.springer.com/book/10.1007...
Excited to see if I can incorporate this text into a data structures (or even discrete maths) course!
My five-project (along with slides, video lectures, etc.) compilers course has all projects now available online free: kmicinski.com/functional-p.... Five projects have you incrementally build a compiler for a substantial language, including functions, mutation, loops, vectors, etc.
Well, if we're just interested in teaching the practical implications of Rice's Theorem & friends, then TMs can be completely dispensed with. Instead, use any of the equivalent models that's closer to practical languages, as exemplified by Jones' Computability and Complexity
"Proving termination and completeness... merely lets you sleep better."
Turns out I'm not alone in this (e.g., found this textbook by Jim Hefferon which I might give it a try in the near future: hefferon.net/computation/). Also looking to try a more semantic treatment of simpler models, using applications from formal methods & verification
been toying with the idea of teaching Theory of Computation by starting with TMs first, where students immediately grapple with important questions like (un)decidability and Rice's Theorem, which nicely motivate simpler computation models that show the expressivity <-> automation tradeoff
A new book on the history of control structures by the creator of #OCaml himself @camlist.bsky.social xavierleroy.org/control-stru...
Interactive theorem provers for proof education. ~ Romina Mahinpei, Manoel Horta Ribeiro, Mae Milano. dl.acm.org/doi/abs/10.1... #ITP #CoqProver #Teaching
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โฆ
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)
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!
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"
