Non-trivial STLC implementation

Stream: new members

[Will Crichton]

Hi folks, I am interested in doing some mechanized proofs about some relatively simple extensions to the simply-typed lambda calculus. Are there any good examples/repositories of reasoning about STLC with at least polymorphic types? I found the examples in the Lean4 docs like "A Certified Type Checker" helpful, but I'm struggling to generalize some of these proof techniques as I add more features.

[Will Crichton]

(Sorry, this is probably more appropriate for the new members channel, but Zulip does not permit me to move the topic...)

[Notification Bot]

This topic was moved here from #lean4 > Non-trivial STLC implementation by Mario Carneiro.

[Mario Carneiro]

This has been done in a few places as an example or the like but I don't have anywhere in particular to point. Maybe you could show what you have and where you got stuck?