Author name cluster

Guy McCusker

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

CSL Conference 2023 Conference Paper

The Functional Machine Calculus II: Semantics

Chris Barrett
Willem Heijltjes
Guy McCusker

The Functional Machine Calculus (FMC), recently introduced by the second author, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects. In this paper, we explore the denotational semantics of the FMC. We have three main contributions: first, we argue that its syntax - in which both effects and lambda-calculus are realised using the same syntactic constructs - is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.

Details

CSL Conference 2018 Conference Paper

On Compositionality of Dinatural Transformations

Guy McCusker
Alessio Santamaria

Natural transformations are ubiquitous in mathematics, logic and computer science. For operations of mixed variance, such as currying and evaluation in the lambda-calculus, Eilenberg and Kelly's notion of extranatural transformation, and often the even more general dinatural transformation, is required. Unfortunately dinaturals are not closed under composition except in special circumstances. This paper presents a new sufficient condition for composability. We propose a generalised notion of dinatural transformation in many variables, and extend the Eilenberg-Kelly account of composition for extranaturals to these transformations. Our main result is that a composition of dinatural transformations which creates no cyclic connections between arguments yields a dinatural transformation. We also extend the classical notion of horizontal composition to our generalized dinaturals and demonstrate that it is associative and has identities.

Details

I&C Journal 2013 Journal Article

Constructing differential categories and deconstructing categories of games

Jim Laird
Giulio Manzonetto
Guy McCusker

Differential categories were introduced by Blute, Cockett and Seely to axiomatize categorically Ehrhard and Regnierʼs syntactic differential operator. We present an abstract construction that takes a symmetric monoidal category and yields a differential category, and show how this construction may be applied to categories of games. In one instance, we recover the category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model, and shows how the differential combinator may be encoded in the imperative language. The second instance corresponds to a new Cartesian differential category of games. We give a model of a simply-typed resource calculus, Resource PCF, in this category and show that it possesses the finite definability property. Comparison with a semantics based on Bucciarelli, Ehrhard and Manzonettoʼs relational model reveals that the latter also possesses this property and is fully abstract.

Details DOI

CSL Conference 2007 Conference Paper

A Games Model of Bunched Implications

Guy McCusker
David J. Pym

Abstract A game semantics of the ( − − *, →)-fragment of the logic of bunched implications, BI, is presented. To date, categorical models of BI have been restricted to two kinds: functor category models; and the category Cat itself. The game model is not of this kind. Rather, it is based on Hyland-Ong-Nickau-style games and embodies a careful analysis of the notions of resource sharing and separation inherent in BI. The key to distinguishing between the additive and multiplicative connectives of BI is a semantic notion of separation. The main result of the paper is that the model is fully complete: every finite, total strategy in the model is the denotation of a term of the αλ -calculus, the term language for the fragment of BI under consideration.

Details

TCS Journal 2003 Journal Article

The regular-language semantics of second-order idealized ALGOL

Dan R. Ghica
Guy McCusker

We explain how recent developments in game semantics can be applied to reasoning about equivalence of terms in a non-trivial fragment of Idealized ALGOL (IA) by expressing sets of complete plays as regular languages. Being derived directly from the fully abstract game semantics for IA, our model inherits its good theoretical properties; in fact, for second-order IA taken as a stand-alone language the regular language model is fully abstract. The method is algorithmic and formal, which makes it suitable for automation. We show how reasoning is carried out using a meta-language of extended regular expressions, a language for which equivalence is decidable.

Details DOI

CSL Conference 2002 Conference Paper

A Fully Abstract Relational Model of Syntactic Control of Interference

Guy McCusker

Abstract Using familiar constructions on the category of monoids, a fully abstract model of Basic SCI is constructed. Basic SCI is a version of Reynolds’s higher-order imperative programming language Idealized Algol, restricted by means of a linear type system so that distinct identifiers are never aliases. The model given here is concretely the same as Reddy’s object spaces model, so this work also shows that Reddy’s model is fully abstract, which was not previously known.

Details

I&C Journal 2000 Journal Article

Games and Full Abstraction for FPC

Guy McCusker

A new category of games is developed which improves over existing such categories in that it interprets sums as well as products, function spaces, and recursive types. A model of FPC, a sequential functional language with just this type structure, is described and shown to be fully abstract.

Details DOI

TCS Journal 1999 Journal Article

Full abstraction for Idealized Algol with passive expressions

Samson Abramsky
Guy McCusker

A fully abstract games model of Reynolds’ Idealized Algol is described. The model gives a semantic account of the distinction between active types, such as commands, which admit side-effecting behaviour, and passive types, such as expressions, which do not.

Details DOI

CSL Conference 1998 Conference Paper

Call-by-Value Games

Samson Abramsky
Guy McCusker

Abstract A general construction of models of call-by-value from models of call-by-name computation is described. The construction makes essential use of the properties of sum types in common denotational models of call-by-name. When applied to categories of games, it yields fully abstract models of the call-by-value functional language PCF v, which can be extended to incorporate recursive types, and of a language with local references as in Standard ML.

Details