О процедурных семантиках строго типизированных функциональных программ

Статья посвящена процедурным семантикам строго типизированных функциональных программ, основанным на алгоритмах интерпретации, которые используют три операции: подстановку, одношаговую $\beta$-редукцию и одношаговую $\delta$-редукцию. Доказывается, что процедурная семантика, основанная на любом из этих алгоритмов интерпретации, непротиворечива. Доказывается также несравнимость процедурных семантик, использующих некоторые алгоритмы интерпретации.