Program and proof optimizations with type systems
scientific article; zbMATH DE number 5362189