Abstract
The last seminar delved into a tricky point in the mechanization of programming languages : the representation of bound variables and the equivalence of terms near renaming of bound variables (alpha-conversion rule). We have reviewed four approaches : de Bruijn indices, where variables are noted by positions instead of names ; Higher-Order Abstract Syntax (HOAS), where metalanguage functions represent object-language linkers ; nominal logics, where the notions of variable names, renaming invariance and quantification on a new name are primitive in logic ; and the " localnameless " approach, which combines de Bruijn indices and nominal approaches. As the POPLmark challenge study showed, each of these approaches has its strengths and weaknesses, and none has established itself as a universal solution.
