Lazy Theories of Operations and Types

摘要

Two foundational systems have been employed to provide the underlying foundations for constructive functional programming (CFP). Neither of these theories was designed with CFP as its major area of application. Our goal is to set the scene for the design of such a theory. This will involve a detailed comparison of the two from the perspective of CFP. The paper contains a series of constructive theories of operations, types and termination, each member of which concentrates upon one particular issue in the design process.