PL theory stuff

Stream: Is there code for X?

[Joachim Breitner]

I might have to play around with a weird program language calculus, with non-trivial binders, reduction rules, contexts etc. I think intuitively I’d reach for Isabelle (its Nominal2 package is great to talk about terms up-to-alpha-equivalence, and get strong induction principles for free) or maybe Coq (because that’s what everyone else is using). But before I do that: How well does Lean fare for PL theory formalization? Any particular good libraries or tools I should be aware of?

[Mario Carneiro]

It doesn't have any particular support specific to PL theory, but the usual stuff with constructing inductive types and inductive predicates and doing cases and induction works well enough, and I have done some nontrivial PL theory stuff in lean (both 3 and 4). I think the situation is fairly similar to Coq formalization, assuming you aren't using one of the big libraries like Iris

[Joachim Breitner]

Thanks. Maybe I’m spoiled a bit, but I appreciate some automation for reasoning up to alpha-equivalence and substitution. Too bad PLT Redex is implemented in Racket and not Lean :-)