Singleton, union, and intersection types for program extraction
scientific article; zbMATH DE number 563083