Pierre-Marie Pédrot

The fire triangle: how to mix substitution, dependent elimination, and effects

2019 · Proceedings of the ACM on Programming Languages

There is a critical tension between substitution, dependent elimination and effects in type theory. In this paper, we crystallize this tension in the form of a no-go theorem that constitutes the fire triangle of type …