Extraction of redundancy-free programs from constructive natural deduction proofs
scientific article; zbMATH DE number 4209628