Ian Mackie

TCS Journal 2017 Journal Article

Logical and Semantic Frameworks with Applications

• Mauricio Ayala-Rincón
• Ian Mackie
• Ugo Montanari

TCS Journal 2010 Journal Article

Gödel’s system T revisited

• Sandra Alves
• Maribel Fernández
• Mário Florido
• Ian Mackie

The linear lambda calculus, where variables are restricted to occur in terms exactly once, has a very weak expressive power: in particular, all functions terminate in linear time. In this paper we consider a simple extension with natural numbers and a restricted iterator: only closed linear functions can be iterated. We show properties of this linear version of Gödel’s T using a closed reduction strategy, and study the class of functions that can be represented. Surprisingly, this linear calculus offers a huge increase in expressive power over previous linear versions of T, which are ‘closed at construction’ rather than ‘closed at reduction’. We show that a linear T with closed reduction is as powerful as T.

CSL Conference 2006 Conference Paper

The Power of Linear Functions

• Sandra Alves
• Maribel Fernández
• Mário Florido
• Ian Mackie

Abstract The linear lambda calculus is very weak in terms of expressive power: in particular, all functions terminate in linear time. In this paper we consider a simple extension with Booleans, natural numbers and a linear iterator. We show properties of this linear version of Gödel’s System \(\mathcal{T}\) and study the class of functions that can be represented. Surprisingly, this linear calculus is extremely expressive: it is as powerful as System \(\mathcal{T}\)

TCS Journal 2003 Journal Article

Operational equivalence for interaction nets

• Maribel Fernández
• Ian Mackie

The notion of contextual (or operational) equivalence is fundamental in the theory of programming languages. By setting up a notion of bisimilarity, and showing that it coincides with contextual equivalence, one obtains a simple coinductive proof technique for showing that two programs are equivalent in all contexts. In this paper we apply these (now standard) techniques to interactions nets, a graphical programming language characterized by local reduction. This work generalizes previous studies of operational equivalence in typed interaction nets since it can be applied to untyped systems, thus all systems of interaction nets are captured.

I&C Journal 2002 Journal Article

Encoding Linear Logic with Interaction Combinators

• Ian Mackie
• Jorge Sousa Pinto

The purpose of this paper is to demonstrate how Lafont's interaction combinators, a system of three symbols and six interaction rules, can be used to encode linear logic. Specifically, we give a translation of the multiplicative, exponential, and additive fragments of linear logic together with a strategy for cut-elimination which can be faithfully simulated. Finally, we show briefly how this encoding can be used for evaluating λ-terms. In addition to offering a very simple, perhaps the simplest, system of rewriting for linear logic and the λ-calculus, the interaction net implementation that we present has been shown by experimental testing to offer a good level of sharing in terms of the number of cut-elimination steps (resp. β-reduction steps). In particular it performs better than all extant finite systems of interaction nets.

TCS Journal 2000 Journal Article

Interaction nets for linear logic

• Ian Mackie

This paper presents a system of interaction nets, a graphical paradigm of computation based on net rewriting, for linear logic. The two main features of the encoding are that the system of interaction is a finite one (meaning that there are a finite number of agents and interaction rules), and most importantly, for the multiplicative exponential fragment we obtain for the first time a strong result that nets in normal form correspond to cut-free proofs – thus we can trivially convert a net back into a proof without a complicated read-back algorithm. For the additives, we perform weak cut-elimination (without the additive commutative cut-elimination step), which is the most natural strategy for these connectives since it avoids unnecessary duplication of proofs. For proofs containing additives, our result is that nets in normal form correspond to cut-free proofs modulo additive commutative cuts. This implementation of linear logic is the most faithful and the most efficient of all the extant interaction net encodings of linear logic.

CSL Conference 1999 Conference Paper

Closed Reductions in the lambda-Calculus

• Maribel Fernández
• Ian Mackie

Abstract Closed reductions in the λ-calculus is a strategy for a calculus of explicit substitutions which overcomes many of the usual syntactical problems of substitution. This is achieved by only moving closed substitutions through certain constructs, which gives a weak form of reduction, but is rich enough to capture the usual strategies in the λ-calculus (call-by-value, call-by-need, etc.) and is adequate for the evaluation of programs. An interesting point is that the calculus permits substitutions to move through abstractions, and reductions are allowed under abstractions, if certain conditions hold. The calculus naturally provides an efficient notion of reduction (with a high degree of sharing), which can easily be implemented.

TCS Journal 1998 Journal Article

Interaction nets and term-rewriting systems

• Maribel Fernández
• Ian Mackie

Term-rewriting systems provide a framework in which it is possible to specify and program in a traditional syntax (oriented equations). Interaction nets, on the other hand, provide a graphical syntax for the same purpose, but can be regarded as being closer to an implementation since the reduction process is local and asynchronous, and all the operations are made explicit, including discarding and copying of data. Our aim is to bridge the gap between the above formalisms by showing how to understand interaction nets in a term-rewriting framework. This allows us to transfer results from one paradigm to the other, deriving syntactical properties of interaction nets from the (well-studied) properties of term-rewriting systems; in particular concerning termination and modularity.