Now showing items 1-6 of 6

  • A Calculus for Access Control in Distributed Systems 

    Abadi, Martin; Burrows, Michael; Lampson, Butler; Plotkin, Gordon (1993)
    We study some of the concepts, protocols, and algorithms for access control in distributed systems, from a logical perspective. We account for how a principal may come to believe that another principal is making a request, ...
  • FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES 

    Abadi, Martin; Pierce, Benjamin; Plotkin, Gordon (2003-11-03)
    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 ...
  • A Logic for Parametric Polymorphism 

    Plotkin, Gordon; Abadi, Martin (2003-11-05)
    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 

    Abadi, Martin; Plotkin, Gordon (2003-11-05)
    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 ...
  • A Per Model of Polymorphism and Recursive Types 

    Abadi, Martin; Plotkin, Gordon (2003-11-05)
    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. ...
  • Subtyping and Parametricity 

    Plotkin, Gordon; Abadi, Martin; Cardelli, Luca (2003-11-05)
    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 ...