up-to-date definition of the formalism behind the language

Stream: lean4

[fishooter]

Hi, I learned lean 4 is based on the calculus of constructions, i.e. https://www.asc.ohio-state.edu/pollard.4/type/readings/coc88.pdf Do you know of some reference where this would be re-written and updated to a modern up-to-date representation for lean4?

[Mario Carneiro]

The standard reference for the type theory of lean is #leantt, with some minor modifications for lean 4 in Sebastian Ullrich 's thesis.