Report on the 2025 Ackermann Award, on behalf of the EACSL Ackermann Award Jury.

Equational reasoning with binders and structural congruence is difficult due to the interaction between name binding and algebraic laws. Equational theories such as commutativity induce forms of permutation invariance on names that are not captured by standard approaches to the formalisation of syntax with binders. We show that in the nominal setting, this limitation can be addressed by using generalised permutation fixed-point constraints to make invariance explicit. This yields a uniform framework for reasoning about equality of nominal terms modulo α-equivalence and arbitrary equational theories. We introduce a proof system and show that it is sound and complete with respect to a nominal-set semantics, which explains how symmetry can be internalised via fixed-point constraints viewed as N-quantified stabiliser conditions. We provide examples in Milner’s π-calculus - a well-known model of concurrent computation that includes binders and non-trivial structural congruences.

Rewriting logic is a logical framework for expressing both concurrent computation and logical deduction using equations and rewrite rules. Quantitative equational reasoning enriches equations with quantitative measures, expressing concepts such as similarity or proximity rather than mere equality of terms. In this article, we bring these two approaches together and propose a quantitative extension of rewriting logic as a flexible formalism for quantitative deduction and computation.

Narrowing extends term rewriting with the ability to search for solutions to equational problems. While first-order rewriting and narrowing are well studied, significant challenges arise in the presence of binders, freshness conditions and equational axioms such as commutativity. This is problematic for applications in programming languages and theorem proving, where reasoning modulo renaming of bound variables, structural congruence, and freshness conditions is needed. To address these issues, we present a framework for nominal rewriting and narrowing modulo equational theories that intrinsically incorporates renaming and freshness conditions. We define and prove a key property called nominal E-coherence under freshness conditions, which characterises normal forms of nominal terms modulo renaming and equational axioms. Building on this, we establish the nominal E-lifting theorem, linking rewriting and narrowing sequences in the nominal setting. This foundational result enables the development of a nominal unification procedure based on equational narrowing, for which we provide a correctness proof. We illustrate the effectiveness of our approach with examples including symbolic differentiation and simplification of first-order formulas.

Equational problems are fundamental in computer science, frequently arising as subproblems across diverse domains, including program analysis and learning from examples and counterexamples. This article focuses on equational problems in languages with binding operators, formulating them within the nominal framework and referring to them as Nominal Equational Problems . We provide a comprehensive definition of solutions for nominal equational problems and introduce a set of simplification rules for computing these solutions within the nominal ground term algebra. We rigorously prove that the simplification rules are sound , solution-preserving and complete . Moreover, we establish that, under a specific strategy for rule application, the simplification process always terminates, thereby providing an effective algorithm for solving nominal equational problems. Finally, we demonstrate the practical relevance of our results by showcasing how nominal equational problems can serve as a framework for learning from examples and counterexamples. We also illustrate their applicability in addressing sufficient completeness problems, emphasising their utility in theoretical and practical contexts.

Abstract Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and $$\alpha $$ α -renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in $$\alpha $$ α -equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the $$\pi $$ π -calculus.

Matching logic is the foundation of the K semantic environment for the specification of programming languages and automated generation of evaluators and verification tools. NLML is a formalization of nominal logic, which facilitates specification and reasoning about languages with binders, as a matching logic theory. Many properties of interest are inductive, and to prove them an induction principle modulo alpha-equality is required. In this paper we show that an alpha-structural Induction Principle for any nominal binding signature can be derived in an extension of NLML with set variables and fixpoint operators. We illustrate the use of the principle to prove properties of the λ-calculus, the computation model underlying functional programming languages. The techniques generalize to other languages with binders. The proofs have been written in and generated using Metamath Zero.

Formalizing languages with binders (such as programming languages and logics) within a logical framework with zero representational distance (i.e., the calculus and its representation look the same) poses non-trivial challenges, including: faithful representation of syntax and binding operators; support for calculus-specific equivalences; faithful representation of the language dynamics (operational semantics); and generation of correct-by-construction implementations. We show how rewriting logic can meet these challenges. More precisely, we show how a general notion of binder signature can be axiomatized in rewriting logic and we propose a general methodology to specify languages with binders, including their structural congruences and operational semantics. We also show how rewriting logic methods provide executable specifications of languages with binders. We use the π -calculus as a running example because it illustrates well the above-mentioned challenges.

As systems evolve, security administrators need to review and update access control policies. Such updates must be carefully controlled due to the risks associated with erroneous or malicious policy changes. We propose a category-based access control (CBAC) model, called Admin-CBAC , to control administrative actions. Since most of the access control models in use nowadays (including the popular RBAC and ABAC models) are instances of CBAC, from Admin-CBAC , we derive administrative models for RBAC and ABAC, too. We present a graph-based representation of Admin-CBAC policies and a formal operational semantics for administrative actions via graph rewriting. We also discuss implementations of Admin-CBAC exploiting the graph-based representation. Using the formal semantics, we show how properties (such as safety, liveness, and effectiveness of policies) and constraints (such as separation of duties) can be checked, and discuss the impact of policy changes. Although the most interesting properties of policies are generally undecidable in dynamic access control models, we identify particular cases where reachability properties are decidable and can be checked using our operational semantics, generalising previous results for RBAC and ABAC α .

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 category-based access control metamodel provides an axiomatic framework for the specification of access control models. In this talk, we give an overview of the category-based approach to access control, obligation and privacy policy specification.

Many service providers offer their services in exchange for users’ private data. Despite new regulations created to protect users privacy, users are often given little choice over the way their data is collected and used. To address privacy concerns in cloud-IoT applications, we propose to use an architecture, called Data Bank, which gives users fine-grained control over their data. Data Bank uses a category-based data access (CBDA) model which covers the whole data life-cycle, from data collection from IoT devices to data sharing with services. We show how dynamic policies can be specified using a new attribute-based instance of CBDA, and describe the use of policy graphs to visualise and analyse policies.

We introduce Nominal Matching Logic (NML) as an extension of Matching Logic with names and binding following the Gabbay-Pitts nominal approach. Matching logic is the foundation of the framework, used to specify programming languages and automatically derive associated tools (compilers, debuggers, model checkers, program verifiers). Matching logic does not include a primitive notion of name binding, though binding operators can be represented via an encoding that internalises the graph of a function from bound names to expressions containing bound names. This approach is sufficient to represent computations involving binding operators, but has not been reconciled with support for inductive reasoning over syntax with binding (e.g., reasoning over λ-terms). Nominal logic is a formal system for reasoning about names and binding, which provides well-behaved and powerful principles for inductive reasoning over syntax with binding, and NML inherits these principles. We discuss design alternatives for the syntax and the semantics of NML, prove meta-theoretical properties and give examples to illustrate its expressive power. In particular, we show how induction principles for λ-terms (α-structural induction) can be defined and used to prove standard properties of the λ-calculus.

We present general notions of access control policy composition using the CBAC model. We show that CBAC provides a uniform framework to define compositions of heterogeneous policies (e.g., RBAC and ABAC policies) as required in many practical situations. Compositions can be built both horizontally (where n given policies are combined to define a new policy) and vertically (where policies are extended by adding administration layers). We show that under some conditions on the operations used to build the composition, it is possible to ensure that the result preserves desirable properties (such as liveness and effectiveness). We also discuss mechanisms to detect and eliminate conflicts that may arise when composing policies originating from different sources.

We present a graph-based language for the specification of administrative access control policies in Admin-CBAC, an administrative model for Category-Based Access Control. More precisely, we propose a multi-level graph representation of policies and a graph-rewriting semantics for administrative actions, from which properties (such as safety, liveness and effectiveness of policies) and constraints (such as separation of duties) can be checked using graph traversal algorithms and rewriting properties. Since Admin-CBAC is a generic model, the techniques are directly applicable to a variety of access control models. In particular, we illustrate our techniques for the RBAC and ABAC instances of Admin-CBAC.

Abstract We define nominal equational problems of the form $$\exists \overline{W} \forall \overline{Y} : P$$ ∃ W ¯ ∀ Y ¯ : P , where $$P$$ P consists of conjunctions and disjunctions of equations $$s\approx _\alpha t$$ s ≈ α t , freshness constraints $$a\#t$$ a # t and their negations: $$s \not \approx _\alpha t$$ s ≉ α t and "Equation missing", where $$a$$ a is an atom and $$s, t$$ s , t nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. These results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo $$\alpha $$ α -equality) is decidable.

Abstract This work extends a rule-based specification of nominal C-unification formalised in Coq to include ‘protected variables’ that cannot be instantiated during the unification process. By introducing protected variables, we are able to reuse the C-unification simplification rules to solve nominal C-matching (as well as equality check) problems. From the algorithmic point of view, this extension is sufficient to obtain a generalised C-unification procedure; however, it cannot be formally checked by simple reuse of the original formalisation. This paper describes the additional effort necessary in order to adapt the specification of the inference rules and reuse previous formalisations. We also generalise a functional recursive nominal C-unification algorithm specified in PVS with protected variables, effectively adapting this algorithm to the tasks of nominal C-matching and nominal equality check. The PVS formalisation is applied to test the correctness of a Python manual implementation of the algorithm.

We present Admin-CBAC, an administrative model for Category- Based Access Control (CBAC). Since most of the access control models in use nowadays are instances of CBAC, in particular the popular RBAC and ABAC models, from Admin-CBAC we derive administrative models for RBAC and ABAC too. We define Admin- CBAC using Barker's metamodel, and use its axiomatic semantics to derive properties of administrative policies. Using an abstract operational semantics for administrative actions, we show how properties (such as safety, liveness and effectiveness of policies) and constraints (such as separation of duties) can be checked, and discuss the impact of policy changes. Although the most interesting properties of policies are generally undecidable in dynamic access control models, we identify particular cases where reachability based properties are decidable and can be checked using our operational semantics, generalising previous results for RBAC and ABACalpha.

We present new algorithms to compute candidate keys and third normal form design of a relational database schema, using strategic port graph rewriting. More precisely, we define port graph rewriting rules and strategies that implement a candidate key definition and Ullman’s algorithm to decompose a relation schema into lossless 3NF schemata. We show the correctness of the resulting database schema by proving soundness, completeness and termination of our strategic graph programs. These rules and strategies provide a declarative and visual description of the algorithms, and permit a fine-grained analysis of the computation steps involved in the normalisation process. The algorithms have been implemented in Porgy, a visual, interactive modelling tool.

We propose a novel data collection and data sharing model for cloud-IoT architectures with an emphasis on data privacy. This model has been implemented in Privasee, an open source platform for privacy-aware web-application development, which provides a plug-in module to support IoT application development. Privasee uses a cloud-IoT architecture called DataBank. We provide examples and discuss future extensions.

We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new $\alpha$-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts. We provide a definition of $\alpha$-equivalence modulo equational theories that take into account A, C and AC theories. Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.

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 propose a cloud-IoT architecture, called Data Bank, aiming at protecting users' sensitive data by allowing them to control which kind of data is transmitted by their devices and providing supportive tools for agreement visualisation and privacy-utility trade-off. The architecture consists of several layers, from IoT objects in the lower layer to web and mobile applications in the top layer, with regulated communication mechanisms to transfer data from the lower level to data processing services in the top level. We illustrate our proposal with an example in a smart vehicle environment.

We present strategic port graph rewriting as a basis for the implementation of visual modelling tools. The goal is to facilitate the specification and programming tasks associated with the modelling of complex systems. A system is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions in the graph. We give a formal semantics for the language, and describe its implementation: the graph transformation and visualisation tool Porgy.

Massive amounts of data are being collected, stored, and analyzed for various business and marketing purposes. While such data analysis is critical for many applications, it could also violate the privacy of individuals. This paper describes the issues involved in designing a privacy aware data management framework for collecting, storing, and analyzing the data. We also discuss behavioral aspects of data sharing as well as aspects of a formal framework based on rewriting rules that encompasses the privacy aware data management framework.

Nominal terms extend first-order terms with nominal features and as such constitute a meta-language for reasoning about the named variables of an object language in the presence of meta-level variables. This article introduces a number of type systems for nominal terms of increasing sophistication and demonstrates their application in the areas of rewriting and equational reasoning. Two simple type systems inspired by Church’s simply typed lambda calculus are presented where only well-typed terms are considered to exist, over which α-equivalence is then axiomatised. The first requires atoms to be strictly annotated whilst the second explores the consequences of a more relaxed de Bruijn-style approach in the presence of atom-capturing substitution. A final type system of richer ML-like polymorphic types is then given in the style of Curry, in which elements of the term language are deemed typeable or not only subsequent to the definition of alpha-equivalence. Principal types are shown to exist and an inference algorithm given to compute them. This system is then used to define two presentations of typed nominal rewriting, one more expressive and one more efficient, the latter also giving rise to a notion of typed nominal equational reasoning.

The Service Oriented Computing (SOC) paradigm is based on service composition, that is, loosely coupled autonomous heterogeneous services, which are collectively composed to implement a particular task. This paper presents a new calculus, called sbCSP, for SOC within the framework of CSP process algebra, showing how services can be defined, invoked, orchestrated and terminated within session hierarchies. We provide operational and denotational trace semantics for the new calculus, and discuss the relationship between the two semantics. We have implemented the extended calculus in FDR (the CSP model checker) and we have used it in a case study to illustrate the expressivity and simplicity of the session model and its reasoning techniques.

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.

Levy's labelled lambda-calculus has played an important role in the understanding of the Geometry of Interaction and its applications to the implementation of lambda-evaluators: labels relate to the multiplicative information of paths. In this article, we generalize the structure of labels, and the underlying term structure, in order to keep track of exponential information too. We first define two-labelled calculi with explicit substitutions and resource management, where labels are in close correspondence with paths in call-by-value and call-by-name translations of the lambda-calculus into Linear Logic proof nets, respectively. We observe a tight relationship between labels and the dynamics of substitutions; this will then guide us through the design of a third calculus that combines the advantages of the previous two, where labels fully reflect the dynamics of substitutions.

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.

We propose an event-based access control model, called Distributed-DEBAC, that takes into account the behaviour of distributed systems. Distributed-DEBAC policies are specified using an algebraic-functional framework. The declarative nature of the model facilitates the analysis of policies, and direct implementations for access control checking even when resources and information are widely dispersed. We give examples of application.

Journal Article Rewriting Corner Get access Maribel Fernández Maribel Fernández Rewriting Corner Editor, King's College London, UK. Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 19, Issue 2, April 2009, Page 261, https://doi.org/10.1093/logcom/exn072 Published: 21 November 2008

We propose an access control model that takes into account the specific behaviour of distributed, highly dynamic environments, and describe their representation using an algebraic-functional framework. The declarative nature of the model facilitates the analysis of policies, and direct implementations for access control checking even when resources and information are widely dispersed.

In large, and often distributed, environments, where access control information may be shared across multiple sites, the combination of individual specifications in order to define a coherent access control policy is of fundamental importance. In order to ensure non-ambiguous behaviour, formal languages, often relying on firstorder logic, have been developed for the description of access control policies. We propose in this paper a formalisation of policy composition by means of term rewriting. We show how, in this setting, we are able to express a wide range of policy combinations and reason about them. Modularity properties of rewrite systems can be used to derive the correctness of the global policy, i.e. that every access request has an answer and this answer is unique

Chris Fox, Maribel Fernandez, Shalom Lappin; Lambda Calculus, Type Theory, and Natural Language II, Journal of Logic and Computation, Volume 18, Issue 2, 1

The integration of first-order and higher-order paradigms has been one of the main challenges in the design of both declarative programming languages and proof environments. It has led to the development of new computation models and new logical frameworks, which have been obtained by enriching first-order rewriting with higher-order capabilities or by adding algebraic features to the λ-calculus.

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.

We present a functional object calculus which solves the traditional conflict between matching-based functional programming and object-oriented programming, by treating uniformly method invocations and functional constructor applications. The key feature of the calculus is that each object remembers its history, that is, the series of method calls that created it. Histories allow us to classify objects in a finer way than classes do. The resulting calculus has a simple syntax and is very expressive; we give examples. Finally, we define a type system for the calculus and show its soundness: typable programs do not produce matching or method-invocation errors

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.

Nominal rewriting extends first-order rewriting with Gabbay-Pitts abstractors: bound entities are named, matching respects α-conversion and can be directly implemented thanks to the use of freshness constraints. In this paper we study two extensions to nominal rewriting. First we introduce a NEW quantifier for modelling name generation and restriction. This allows us to model higher-order functions involving local state, and has also applications in concurrency theory. The second extension introduces new constraints in freshness contexts. This allows us to express strategies of reduction and has applications in programming language design and implementation. Finally, we study confluence properties of nominal rewriting and its extensions.

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.

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.

In this paper we present the algebraic-λ-cube, an extension of Barendregt's λ-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular property of all the systems in the algebraic-λ-cube, provided that the first-order rewrite rules are non-duplicating and the higher-order rules satisfy the general schema of Jouannaud and Okada. We also prove that local confluence is a modular property of all the systems in the algebraic-λ-cube, provided that the higher-order rules do not introduce critical pairs. This property and the strong normalization result imply the modularity of confluence.

Presents the algebraic-/spl lambda/-cube, an extension of Barendregt's (1991) /spl lambda/-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular property of all systems in the algebraic-/spl lambda/-cube, provided that the first-order rewrite rules are non-duplicating and the higher-order rules satisfy the general schema of Jouannaud and Okada (1991). This result is proven for the algebraic extension of the calculus of constructions, which contains all the systems of the algebraic-/spl lambda/-cube. We also prove that local confluence is a modular property of all the systems in the algebraic-/spl lambda/-cube, provided that the higher-order rules do not introduce critical pairs. This property and the strong normalization result imply the modularity of confluence.>