Simply typed lambda calculus

Stream: computer science

[Fabrizio Montesi]

@Chris Henson I'm probably gonna make multiple reviews here: https://github.com/cs-lean/cslib/pull/17

So that you don't get a huge amount of comments all at once. :⁠-⁠)

[Fabrizio Montesi]

Done reviewing, phew! :) Great work!

The locally nameless representation is kinda neat.

[Chris Henson]

Thanks! I've addressed the last round of comments.

[Fabrizio Montesi]

Merged. Locally nameless simply-typed lambda calculus is in the house!

[Chris Henson]

Nice, thanks for the work reviewing!

[Chris Henson]

I think I will tackle System F next. Probably will take me a little longer than my previous PRs because those I had done some work on previously in my personal repos. I also want to think about if we can do anything to make logical relations stuff reusable for strong normalization proofs.

[Fabrizio Montesi]

Logical relations are useful in concurrency as well so it'd be interesting to look at, indeed. Let me know if/when you wanna discuss that.