Now showing items 1-20 of 32

  • Abstract Syntax and Variable Binding (Extended Abstract) 

    Fiore, Marcelo P; Plotkin, Gordon; Turi, Daniele (2003-11-06)
    We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The ...
  • Adequacy for Algebraic Effects 

    Plotkin, Gordon; Power, John (SPRINGER-VERLAG, 2002)
    Moggi proposed a monadic account of computational effects. He also presented the computational lamda-calculus, c, a core call-by-value functional programming language for effects; the effects are obtained by adding ...
  • An Axiomatisation of Computationally Adequate Domain Theoretic Models of FPC 

    Fiore, Marcelo P; Plotkin, Gordon (1994)
    Categorical models of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types) are defined. Then, domain-theoretic models of FPC are axiomatised and a wide subclass of them —the ...
  • Bialgebraic Semantics and Recursion 

    Plotkin, Gordon (Elsevier Science, 2001)
    In [9] a unifying framework was given for operational and denotational semantics. It uses bialgebras, which are combinations of algebras (used for syn- tax and denotational semantics) and coalgebras (used for operational ...
  • Combining computational effects: commutativity and sum 

    Hyland, Martin; Plotkin, Gordon; Power, John (2003-11-05)
    We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi’s paradigm for modelling ...
  • Complete Cuboidal Sets in Axiomatic Domain Theory (Extended Abstract) 

    Fiore, Marcelo P; Plotkin, Gordon; Power, John (2003-11-06)
    We study the enrichment of models of axiomatic do- main theory. To this end, we introduce a new and broader notion of domain, viz. that of complete cuboidal set, that complies with the axiomatic requirements. We show ...
  • Computational effects and operations: an overview 

    Plotkin, Gordon; Power, John (2002)
    We overview a programme to provide a unified semantics for computational effects based upon the notion of a countable enriched Lawvere theory. We define the notion of countable enriched Lawvere theory, show how the various ...
  • Concrete Domains 

    Kahn, Gilles; Plotkin, Gordon (1993)
    This paper introduces the theory of a particular kind of computation domains called concrete domains. The purpose of this theory is to find a satisfactory framework for the notions of coroutine computation and sequentiality ...
  • Configuration Structures 

    van Glabbeek, R.J. (2003-11-05)
    In this paper the correspondence between safe Petri nets and event structures, due to Nielsen, Plotkin and Winskel, is extended to arbitrary nets without self-loops, under the collective token interpretation. To this ...
  • An Extension of Models of Axiomatic Domain Theory to Models of Synthetic Domain Theory 

    Plotkin, Gordon; Fiore, Marcelo P (2003-11-05)
    We relate certain models of Axiomatic Domain Theory (ADT) and Synthetic Domain Theory (SDT). On the one hand, we introduce a class of non-elementary models of SDT and show that the domains in them yield models of ADT. ...
  • 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 Framework for Defining Logics 

    Plotkin, Gordon; Honsell, Furio; Harper, Robert (ASSOC COMPUTING MACHINERY, NEW YORK, 1993)
    The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated ...
  • From Action Calculi to Linear Logic 

    Barber, Andrew G; Gardner, Phillipa; Hasegawa, Masahito; Plotkin, Gordon (SPRINGER-VERLAG, 1998)
    Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types paradigm; the type theory has a ...
  • Full Abstraction, Totality and PCF 

    Plotkin, Gordon (2003-11-06)
    Inspired by a question of Riecke, we consider the interaction of totality and full abstraction, asking whether full abstraction holds for Scott’s model of cpos and continuous functions if one restricts to total programs ...
  • An Illative Theory of Relations 

    Plotkin, Gordon (2003-11-03)
    In a previous paper an intensional theory of relations was formulated [Plo90]. It was intended as a formalisation of some of the ideas of Situation Theory concerning relations, assignments, states-of-a airs and facts; ...
  • Lax Logical Relations 

    Plotkin, Gordon; Power, John; Sannella, Donald; Tennent, Robert (SPRINGER-VERLAG, 2000)
    Lax logical relations are a categorical generalisation of logical relations; though they preserve product types, they need not preserve exponential types. But, like logical relations, they are preserved by the meanings ...
  • 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 ...
  • Logical Full Abstraction and PCF 

    Longley, John R; Plotkin, Gordon (2000)
    We introduce the concept of logical full abstraction, generalising the usual equational notion. We consider the language PCF and two extensions with “parallel” operations. The main result is that, for standard ...
  • 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 ...
  • Notions of Computation Determine Monads 

    Plotkin, Gordon; Power, John (SPRINGER-VERLAG, 2002)
    We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of pri- mary interest that have been used to model computational e ects, with the striking ...