## Search

Now showing items 21-30 of 34

#### Bistructures, Bidomains and Linear Logic

(MIT Press, 2000-05)

Bistructures are a generalisation of event structures which allow
a representation of spaces of functions at higher types in an order-extensional setting. The partial order of causal dependency is replaced
by two orders, ...

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

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

#### On a Question of H. Friedman

(ACADEMIC PRESS INC, 1996)

In this paper we answer a question of Friedman, providing an ω-separable
model M of the λβη-calculus. There therefore exists an α-separable model for
any α≥0. The model M permits no non-trivial enrichment as a partial ...

#### Logical Full Abstraction and PCF

(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 Per Model of Polymorphism and Recursive Types

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

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