Simple Type Theory definitions & Theorems

Stream: Type theory

[Philogy]

I was wondering if anyone had resources or examples on how to define & make theorems around simple type systems, the like you'd find in the TAPL (Types and Programming Languages) book, in Lean4.

I'm a beginner self teaching in the topic and am trying to mess around with my own type theories and would love a more concrete way of defining & proving theorems in them, I'm just not sure what an idiomatic way to define a "type system" in Lean4 would be as the starting point.

[Sebastian Miele]

I guess Software Foundations, in particular Volume 2, also by Benjamin C. Pierce (and others), is a canonical resource on that. It uses Rocq, but at least most techniques should work very similarly in Lean. See also #new members > Self-studying Lean4 with Software Foundations? and #general > Working on a Translation of Software Foundations to LEAN.

[Chris Henson]

In CSLib we have examples of both simples types and system F with subtyping: https://github.com/leanprover/cslib/tree/main/Cslib/Languages/LambdaCalculus/LocallyNameless. There are proofs of at least progress/preservation for each.

These all currently use a locally nameless representation of syntax where bound and free variables are syntactically differentiated. There are other styles you should look into, like well-scoped indices where terms are indexed by the number of free variables. (We will have this soon, but maybe others have an example in the meantime)

[Chris Henson]

A while ago I wrote a blog post Beginner Resources for Formalizing Lambda Calculi you might find helpful. It collects links to various examples in different proof assistants.

[Philogy]

Chris Henson said:

A while ago I wrote a blog post Beginner Resources for Formalizing Lambda Calculi you might find helpful. It collects links to various examples in different proof assistants.

thanks!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

There is also the hitchhiker's guide which considers operational and denotational semantics.