Kristopher Micinski

btw, I also have a visualizer for natural deduction proof trees (kmicinski.com/cis352-s26/p...) which do include type theory variants. Let me know if you think there's any potential harmony here.

yeah I think adding typed lambda calculi should be easy, but I think seeing reductions for those is perhaps not *as* relevant because it's the same thing as just erasing the types(?). Are there any cases of term rewriting systems for typed languages (maybe, say, CIC?) where you think this would help

thanks for the tip, will try it out!

viz of reduction sequence in the tutorial

options menu with a huge lambda calculus term in the background being gradually reduced.

a self-loop for the omega combinator in the tutorial.

illustrating the church-rosser property.

Latest in my educational apps for learning programming languages: an interactive tutorial / visualizer for reduction in the untyped λ-calculus. Now live online at kmicinski.com/cis352-s26/l... (git repo at: github.com/kmicinski/la...).

thanks Patrick, I also have some recent notes on this: kmicinski.com/cis352-s26/c..., this also links to a playground for natural deduction which I made the other night: kmicinski.com/cis352-s26/p...

mostly i agree but I found having the LLM copy-edit my papers has been a huge time saver. I find some words that were not misspelled words but the wrong word

Also you won’t have the dean in your office complaining about you telling people to go fuck themselves

lmao no way in my case the students are just like "wow this class sucks and honestly the whole topic sucks why aren't we learning javascript"

Programming with Algebra (Course Notes) kmicinski.com/cis352-s26/a...

Given the fact that so many thoughtful people in the world are just insisting that AI can do everything and has no flaws, I think it is fair to say that finally all of the former adults in the room are tripping balls. I am a big AI fan myself of course.

New on my Modern Deduction blog: "Post 3: Data-Parallel Functional Programming in Datalog"
kmicinski.com/modern-deduc...

Good question, I think a bit of both but of course, I don’t have a better answer than you I expect

New on my blog: "Why Study CS? Thoughts on LLM-assisted software engineering" kmicinski.com/claude-code-...

People never understand when I wear the ”I’m with stupid” shirt by myself 😭

A rose by any other name! 🥀

A good friend of mine is now a research scientist at CrowdStrike after leaving a government-adjacent job (after whole team got fired). Occasionally I text him and I'm like "oh hey did you guys bring down the internet" and he writes "no no, you're thinking CloudFlare today--we were three weeks ago"

(very aggressively Bsky-style post): "where are these people when it comes to background checks!?"

To be honest, I don't think any culture understands the concept of acceptable losses quite like the USA

Totally agreed with everything you said, but I also have a huge bank of exam questions so making a separate exam has not been too touch recently. In the case of a coding exam, I can see where time limitations would be an issue because debugging can just take forever.

OTOH, while I strongly support access to accommodations for the disabled, I am inclined to agree that 40% indicates something is going wrong. I just find the recent discourse about this to be .. groan.. because it just seems like more memes of the shitty fascism-embracing vibe configuration of 2025.

right, ok--I can believe that one. I can pretty confidently (I have intentionally studied this, but not in a scientific manner) say that accommodations have changed an outcome in literally zero instances of my class. I too felt annoyed by them in principle when I started teaching but it was nbd

Maybe my exams aren’t hard enough. I dunno. I find most students finish around the 1/2-2/3 time mark, and nobody is really limited by time in the sense that another hour would change B->B+ or something. I agree, exams shouldn’t be time-limited, in the presence of extra time it could be unfair.

Tbh I just haven’t had any issue implementing the thing Sam says is hard. I’ve had multiple classes of nearly 100 people and at the end, almost nobody is there. I asked a few why they stayed and it was universally just checking answers or contemplating more. Sam might be right but it’s not my exp.

something about @krismicinski.bsky.social getting an f150 or the like

now Ford is paying *me*: notice the official Ford color palette being used in this shot.

I’ve got a new course I worked on, my first time running it! Looked at material from both of you. kmicinski.com/functional-p...

@krismicinski's build a compiler in Five Projects

Link to the blog post by @krismicinski.bsky.social: kmicinski.com/functional-p...

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.

YouTube video by Kristopher Micinski Closure Conversion: Examples and Implementation

[58min] "Closure Conversion: Examples and Implementation" I explain the intuition for closure conversion, show some examples, and then code up an implementation of bottom-up closure conversion in Racket meant to be used in my compilers' class. www.youtube.com/watch?v=zMta...