Mathematically Structured but not Necessarily Functional Programming (Extended Abstract)
Andrej Bauer · 2008
Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions as types, because it allows the realizers to use computational eects such as non-termination,