Now showing items 1-5 of 5
A Logic for Parametric Polymorphism
In this paper we introduce a logic for parametric polymorphism. Just as LCF is a logic for the simply-typed -calculus with recursion and arithmetic, our logic is a logic for System F. The logic permits the formal ...
A Logical View of Composition
We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification approaches; one of the logics ...
FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES
We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit between models and programming ...
Subtyping and Parametricity
In this paper we study the interaction of subtyping and parametricity. We describe a logic for a programming language with parametric polymorphism and subtyping. The logic supports the formal definition and use of ...
A Per Model of Polymorphism and Recursive Types
A model of Reynolds’ polymorphic lambda calculus is provided, which also allows the recursive definition of elements and types. The technique is to use a good class of partial equivalence relations over a certain cpo. ...