A type-based HFL model checking algorithm
scientific article; zbMATH DE number 7834968