Lambda Calculus and its variations

Stream: Is there code for X?

[Sehun Kim]

Is there a lambda calculus or related formalizations, such as simply typed lambda calculus, in Mathlib? I found a similar discussion relating them to category theory, but nobody answered.

I also want to know whether there is any basic type theory in Mathlib, or even bootstrapping theorems about Lean expressions themselves.

Is there a standard way to represent lambda expressions? Since symbols such as $\lambda$, $\forall$, and : are reserved for Lean’s own syntax, I would like to know whether there is a conventional alternative notation when bootstrapping expressions. I assume that, if it exists, it would fall under logic or model theory, but I could not find anything.

[Snir Broshi]

I believe #CSLib has STLC

[Snir Broshi]

For type theory you might be interested in lean4lean

[Chris Henson]

Snir Broshi said:

I believe #CSLib has STLC

CSLib has both STLC and System F with subtyping so far.

[Chris Henson]

Regarding notation, I haven't invested much time into it in CSLib. There are some obscure Unicode alternatives to some of the symbols. You can also take the approach of doing a more proper quasioquote DSL, see this blog post for example.

[Sehun Kim]

Thanks a lot. I heard CSLib before but I couldn't think of looking for it.