1 paper
Nathanaëlle Courant, Xavier Leroy
Convertibility checking - determining whether two lambda-terms are equal up to reductions - is a crucial component of proof assistants and dependently-typed languages. Practical im…