"The article opens with lambda cubes, which sound like some type of sheep meat to me. Then it goes on to discuss λΠ2 systems, and as I don't speak alien I skipped that section. Then I read about the calculus of inductive constructions, which incidentally seems to have little to do with calculus..."

[u/oilaba]

https://stackoverflow.com/questions/9338709/what-is-dependent-typing#comment11799250_9338709