## Search

Now showing items 1-10 of 10

#### A Semantics for Static Type Inference

(SPRINGER VERLAG, 1991)

Curry’s system for F-deducibility is the basis for static type inference
algorithms for programming languages such as ML. If a natural
“preservation of types by conversion” rule is added to Curry’s system, it
becomes ...

#### On Functors Expressible in the Polymorphic Typed Lambda Calculus

(Information and Computation, 1991)

Given a model of the polymorphic typed lambda calculus based upon a Cartesian
closed category K, there will be functors from K to K whose action on objects can be
expressed by type expressions and whose action on morphisms ...

#### A Calculus for Access Control in Distributed Systems

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

#### Full completeness of the multiplicative linear logic of Chu spaces

(1999)

We prove full completeness of multiplicative linear logic
(MLL) without MIX under the Chu interpretation. In particular
we show that the cut-free proofs of MLL theorems
are in a natural bijection with the binary logical ...

#### An Axiomatisation of Computationally Adequate Domain Theoretic Models of FPC

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

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

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

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