## Search

Now showing items 21-30 of 34

#### Combining computational effects: commutativity and sum

(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 ...

#### Concrete Domains

(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 ...

#### Uncountable Limits and the Lambda Calculus

(Publishing Association Nordic Journal of Computing, 1995)

In this paper we address the problem of solving recursive domain
equations using uncountable limits of domains. These arise for instance, when
dealing with the omega_1-continuous function-space constructor and are used ...

#### Type Theory and Recursion Extended Abstract

(2003-11-05)

At first sight, type theory and recursion are compatible: there are many models of the typed lambda
calculus with a recursion operator at all types. However the situation changes as soon as one considers
sums. By a theorem ...

#### Subtyping and Parametricity

(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 ...

#### Towards a Mathematical Operational Semantics

(2003-11-05)

We present a categorical theory of ‘well-behaved’
operational semantics which aims at complementing
the established theory of domains and denotational semantics to form a coherent whole. It is shown that, if
the operational ...

#### A Set-Theoretical Definition of Application

(2003-11-05)

This paper is in two parts. Part 1 is the previously unpublished 1972 memorandum [41], with editorial changes and some minor corrections. Part 2
presents what happened next, together with some further development of
the ...

#### A Framework for Defining Logics

(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

(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 ...

#### Semantics for algebraic operations

(KLUWER ACADEMIC PUBL, 2003)

Given a category C with finite products and a strong monad T on C, we investigate axioms under which an ObC-indexed family of operations of the form α_x : (Tx)n ! Tx provides a definitive semantics for algebraic operations ...