We present hierarchical higher-order port graphs ( <?TeX $\mathbb {H}$?> Math 1 oP) and a notion of strategic <?TeX $\mathbb {H}$?> Math 2 oP-rewriting, as a foundation for modelling tools. To illustrate the methodology we provide a specification of the lambda-calculus, the computation model underlying the functional programming paradigm. We give a categorical semantics for <?TeX $\mathbb {H}$?> Math 3 oP-rewriting following the Single Pushout approach, by generalising Löwe’s notion of graph structure. We also discuss simple extensions of strategy languages to take into account the hierarchical structure of <?TeX $\mathbb {H}$?> Math 4 oP.

The Attribute-Based Access Control (ABAC) model is one of the most powerful access control models in use. It subsumes popular models, such as the Role-Based Access Control (RBAC) model, and can also enforce dynamic policies where authorisations depend on values of user, resource or environment attributes. However, in its general form, ABAC does not lend itself well to some operations, such as review queries, and ABAC policies are in general more difficult to specify and analyse than simpler RBAC policies. In this paper we propose a formal specification of ABAC in the category-based metamodel of access control, which adds structure to ABAC policies, making them easier to design and understand. We provide an axiomatic and an operational semantics for ABAC policies, and show how to use them to analyse policies and evaluate review queries.

We investigate numeral systems in the lambda calculus; specifically in the linear lambda calculus where terms cannot be copied or erased. Our interest is threefold: representing numbers in the linear calculus, finding constant time arithmetic operations when possible for successor, addition and predecessor, and finally, efficiently encoding subtraction—an operation that is problematic in many numeral systems. This paper defines systems that address these points, and in addition provides a characterisation of linear numeral systems.

In this article we discuss three different notions of linearity: syntactical, operational and denotational. We briefly define each notion of linearity, pointing out some of the main results in the area, and describe applications of linear languages and type systems.

Journal Article Linearity in Computation Get access Mário Florido, Mário Florido Search for other works by this author on: Oxford Academic Google Scholar Ian Mackie Ian Mackie Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 24, Issue 3, June 2014, Pages 511–512, https://doi.org/10.1093/logcom/exs024 Published: 12 June 2012

We show that the full PCF language can be encoded in L_rec, a syntactically linear λ-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for L_rec, exploiting its linearity.

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 Godel'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.

The dichotomy between programs and data projects itself onto two paradigms in software visualisation: programs are visualised by program animation, and data is visualised by algorithm animation. We put forward a programming paradigm where, like functional or logic programming, and some rewriting paradigms, programs and data are represented at the same level - program are just one particular kind of data. Animation of these programs/algorithms breaks the dichotomy and leads to an alternative perspective on visualisation. Our paradigm is a graphical one, and thus is exceptionally well suited for visualisation.

This second special issue devoted to ‘developments in computational models’ (the first was Volume 16 Issue 4) came out of an open call for papers following the First International Workshop on Developments in Computational Models (DCM). This took place in Lisbon, Portugal, on the 10th July 2005, and was a satellite event of ICALP 2005 focused on abstract models of computation and their associated programming paradigms.

Term graph rewriting is concerned with the representation of functional expressions as graphs and the evaluation of these expressions by rule-based graph transformation. The advantage of computing with graphs rather than terms is that common subexpressions can be shared, improving the efficiency of computations in space and time. Sharing is ubiquitous in implementations of programming languages: many functional, logic, object-oriented and concurrent calculi are implemented using term graphs.

In recent years several new models of computation have emerged that have been inspired by the physical sciences, biology and logic, to name but a few (for example, quantum computing, chemical machines and bio-computing). Also, many developments of traditional computational models have been proposed with the aim of taking into account the new demands of computer systems users and the new capabilities of computation engines.

Interaction nets provide a graphical paradigm of computation based on net rewriting. They have proved most successful in understanding the dynamics of reduction in the λ-calculus, where very efficient evaluators have been obtained. Most work in this area is heavily based on the pure λ-calculus, and a general theory of coding data structures with interaction nets has not been forthcoming. The purpose of this paper is to show how all of these systems encoding the λ-calculus can be extended to work with different kinds of data structures, which is a first step towards using these evaluators as the basis of implementation of a richer programming language.

Starting from the -calculus. Moreover, since substitutions can move through abstractions and reductions are allowed under abstractions (if certain conditions hold), closed reduction naturally provides an efficient notion of reduction with a high degree of sharing and low overheads. We present a family of abstract machines for closed reduction. Our benchmarks show that closed reduction performs better than all standard weak strategies, and its low overheads make it more efficient than optimal reduction in many cases.

We present a generalisation of first-order rewriting which allows us to deal with terms involving binding operations in an elegant and practical way. We use a nominal approach to binding, in which bound entities are explicitly named (rather than using a nameless syntax such as de Bruijn indices), yet we get a rewriting formalism which respects α-conversion and can be directly implemented. This is achieved by adapting to the rewriting framework the powerful techniques developed by Pitts et al. in the FreshML project.Nominal rewriting can be seen as higher-order rewriting with a first-order syntax and built-in α-conversion. We show that standard (first-order) rewriting is a particular case of nominal rewriting, and that very expressive higher-order systems such as Klop's Combinatory Reduction Systems can be easily defined as nominal rewriting systems. Finally we study confluence properties of nominal rewriting.

Interaction nets provide a graphical paradigm of computation based on net rewriting. They have proved most successful in understanding the dynamics of reduction in the λ-calculus, where the prime example is the implementation of optimal reduction for the λ-calculus (Lamping's algorithm), given by Gonthier, Abadi and Lévy. However, efficient implementations of optimal reduction have had to break away from the interaction net paradigm. In this paper we give a new efficient interaction net encoding of the λ-calculus which is not optimal, but overcomes the inefficiencies caused by the bookkeeping operations in the implementations of optimal reduction. We believe that this implementation of the λ-calculus could provide the basis for highly efficient implementations of functional languages.

In this paper we study a notion of operational equivalence for interaction nets, following the recent success of applying methods based on bisimulation to functional and object oriented programming languages. We set up notions of contextual equivalence and bisimilarity and show that they coincide. A coinduction principle then gives a simple and robust way of showing when two interaction nets are contextually equivalent. We include several examples to demonstrate the usefulness of the approach, in particular for optimizing interaction nets.

Interaction nets provide a graphical paradigm of computation based on net rewriting. By encoding the cut-elimination process of linear logic they have proved successful in understanding the dynamics of reduction in the /spl lambda/-calculus. G. Gonthier et al. (1992) gave an optimal infinite system of interaction nets for linear logic by removing the global boxes. However efficient implementations of optimal reduction have had to break away from the interaction net paradigm. Here we give an efficient new finite interaction net encoding of linear logic which is not optimal, but overcomes many of the inefficiencies caused by the bookkeeping operations in the implementations of optimal reduction. We code the global operations on boxes (contraction, weakening, dereliction, commutative cut) in a local way, keeping the box structure, which results in a system allowing a great deal of sharing with an extremely low overhead. We believe that this implementation is the most faithful of all the extant interaction net encodings of linear logic.

We investigate implementation techniques arising directly from Girard's Geometry of Interaction semantics for Linear Logic, specifically for a simple functional programming language (PCF). This gives rise to a very simple, compact, compilation schema and run-time system. We analyse various properties of this kind of computation that suggest substantial optimisations that could make this paradigm of implementation not only practical, but potentially more efficient than extant paradigms.

Abstract We take Abramsky's term assignment for Intuitionistic Linear Logic (the linear term calculus) as the basis of a functional programming language. This is a language where the programmer must embed explicitly the resource and control information of an algorithm. We give a type reconstruction algorithm for our language in the style of Milner's W algorithm, together with a description of the implementation and examples of use.