Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
scientific article; zbMATH DE number 1394791