Zulip Chat Archive

Stream: new members

Topic: Non-trivial STLC implementation

Will Crichton (Jun 16 2023 at 00:14):

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 (Jun 16 2023 at 00:46):

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

Notification Bot (Jun 16 2023 at 00:53):

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

Mario Carneiro (Jun 16 2023 at 00:55):

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?

Last updated: Dec 20 2023 at 11:08 UTC