A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
scientific article; zbMATH DE number 6154937