Abstract :
The author develops an operational model of an impredicative version of explicit polymorphism, namely, an extension of the second-order lambda-calculus, including a fixed-point combinator and a multisorted first-order algebra. He shows that the typical properties of the lambda -calculus are preserved, and he investigates novel aspects that arise from second-order type structure as well as the relationships with well-known, simply typed, PCF-like languages. A suitable theory of observably equivalent terms is defined, and its complexity is explored. A denotional model suggesting interesting extensions of a language is studied.<>
Keywords :
programming languages; programming theory; PCF-like languages; combinator; denotional model; explicit polymorphism; fixed point; models; observable equivalences; second order lambda-calculus; Algebra; Calculus; Formal verification; Functional programming; Logic; Programming profession; Prototypes; Software prototyping; Standardization; Topology;
