Game semantics describe the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterise definable strategies, that is, strategies that actually behave like a proof. This is usually done by restricting the model to strategies satisfying subtle combinatorial conditions, whose preservation under composition is often difficult to show. In this paper we present an original methodology to achieve this task, which requires a combination of advanced tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of the monoidal category of definable strategies of our model using generators and relations: these strategies can be generated from a finite set of atomic strategies, and the equality between strategies admits a finite axiomatisation, and this equational structure corresponds to a polarised variation of the bialgebra notion. The work described in this paper thus forms a bridge between algebra and denotational semantics in order to reveal the structure of dependencies induced by first-order quantifiers, and lays the foundations for a mechanised analysis of causality in programming languages.

This paper gives the first proof that the subtyping relation of a higher-order lambda calculus, ${\cal F}^{\omega}_{\leq}$, is anti-symmetric, establishing in the process that the subtyping relation is a partial order – reflexive, transitive, and anti-symmetric up to $\beta$-equality. While a subtyping relation is reflexive and transitive by definition, anti-symmetry is a derived property. The result, which may seem obvious to the non-expert, is technically challenging, and had been an open problem for almost a decade. In this context, typed operational semantics for subtyping, and the logical relation used to prove its equivalence with the declarative presentation of ${\cal F}^{\omega}_{\leq}$, offers a powerful new technology to solve the problem: of particular importance is our extended rule for the well-formedness of types with head variables. The paper also gives a presentation of ${\cal F}^{\omega}_{\leq}$ without a relation for $\beta$-equality, which is apparently the first such, and shows its equivalence with the traditional presentation.

We discuss some recent results related to the deduction of a suitable probabilistic model for the description of the statistical features of a given deterministic dynamics. More precisely, we motivate and investigate the computability of invariant measures and some related concepts. We also present some experiments investigating the limits of naive simulations in dynamics.

In (hyper)coherence semantics, proofs/terms are cliques in (hyper)graphs. Intuitively, the vertices represent the results of computations and the edge relation witnesses the ability to carry out the computation assembled into a single piece of data or a single (strongly) stable function, at arrow types.

In (hyper)coherence semantics, the argument of a (strongly) stable functional is always a (strongly) stable function. As a consequence, compared to the relational semantics where there is no edge relation, some vertices are missing. Recovering these vertices is essential if we are to reconstruct proofs/terms from their interpretations. It will also be useful for comparing with other semantics, such as game semantics.

Bucciarelli and Ehrhard (2001) introduced a non-uniform coherence space semantics, where no vertex is missing. By constructing the co-free exponential, we get a new version of this semantics, together with non-uniform versions of hypercoherences and multicoherences. This provides a new semantics in which an edge is a finite multiset. Thanks to the co-free construction, these non-uniform semantics are deterministic in the sense that the intersection of a clique and an anti-clique contains at most one vertex, which is a result of interaction, and they then extensionally collapse onto the corresponding uniform semantics.

The function of airport gate assignment is to assign appropriate gates for arrival and departure flights and to ensure the flights are on schedule. A key task of airport ground operations is assigning the airport gate with high efficiency and a reasonable arrangement. In this paper we establish an optimised model based on the characteristics of both the flights (the flight type, flight down time and the number of passengers) and the airport gates (the ease of access of the airport gate). We give a representation of the solution space and a direct graph model of the airport gate configuration based on dynamic scheduling parallel machines. We design a method for solving the airport gate configuration based on an immune genetic algorithm. The simulation results show the effectiveness of this model and algorithm.

We apply the categorical properties of polymorphic functions to compile-time analysis, specifically projection-based strictness analysis. First we interpret parameterised types as functors in a suitable category, and show that they preserve monics and epics. Then we define “strong” and “weak” polymorphism, the latter admitting certain projections that are not polymorphic in the usual sense. We prove that, under the right conditions, a weakly polymorphic function is characterised by a single instance. It follows that the strictness analysis of one simple instance of a polymorphic function yields results that apply to all. We show how this theory may be applied. In comparison with earlier polymorphic strictness analysis methods, ours can apply polymorphic information to a particular instance very simply. The categorical approach simplifies our proofs, enabling them to be carried out at a higher level, and making them independent of the precise form of the programming language to be analysed. The major limitation of our results is that they apply only to first-order functions.

Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe’s method in the Beluga formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of Beluga’s support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in Beluga’s reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives Beluga provides. We believe that this mechanization is a significant example that illustrates Beluga’s strength at mechanizing challenging (co)inductive proofs using HOAS encodings.

We consider the well-known Coordinated Attack Problem, where two generals have to decide on a common attack, when their messengers can be captured by the enemy. Informally, this problem represents the difficulties to agree in the presence of communication faults. We consider here only omission faults (loss of message), but contrary to previous studies, we do not to restrict the way messages can be lost, i.e., we make no specific assumption, we use no specific failure metric. In the large subclass of message adversaries where the double simultaneous omission can never happen, we characterize which ones are obstructions for the Coordinated Attack Problem. We give two proofs of this result. One is combinatorial and uses the classical bivalency technique for the necessary condition. The second is topological and uses simplicial complexes to prove the necessary condition. We also present two different Consensus algorithms that are combinatorial (resp. topological) in essence. Finally, we analyze the two proofs and illustrate the relationship between the combinatorial approach and the topological approach in the very general case of message adversaries. We show that the topological characterization gives a clearer explanation of why some message adversaries are obstructions or not. This result is a convincing illustration of the power of topological tools for distributed computability.

We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Löf type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.

We study the reduction in a $\lambda$ -calculus derived from Moggi’s computational one, which we call the computational core. The reduction relation consists of rules obtained by orienting three monadic laws. Such laws, in particular associativity and identity, introduce intricacies in the operational analysis. We investigate the central notions of returning a value versus having a normal form and address the question of normalizing strategies. Our analysis relies on factorization results.

Behavioural equivalences are a means of establishing whether computing systems possess the same properties. The specific set of properties that are preserved by a specific behavioural equivalence clearly depends on how the system behaviour is observed and can usually be characterised by means of a modal logic. In this paper we consider three different approaches to the definition of behavioural equivalences – bisimulation, testing and trace – applied to three different classes of systems – non-deterministic, probabilistic and Markovian – and we survey the nine resulting modal logic characterisations, each of which stems from the Hennessy–Milner logic. We then compare the nine characterisations with respect to the logical operators, in order to emphasise the differences between the three approaches in the definition of behavioural equivalences and the regularities within each of them. In the probabilistic and Markovian cases we also address the issue of whether the probabilistic and temporal aspects should be treated in a local or global way and consequently whether the modal logic interpretation should be qualitative or quantitative.

We consider a class of uncertain non-linear systems preceded by unknown backlash-like hysteresis, which is modelled by a differential equation. We propose a new state feedback robust adaptive control scheme using a backstepping technique and properties of the differential equation. In this control scheme, we construct a new continuous function to design an estimator to estimate the unknown constant parameters and the unknown bound of a ‘disturbance-like’ term. The transient performance of the output tracking error can be guaranteed by the introduction of pre-estimates of the unknown parameters in our controller together with update laws. We do not require bounds on the ‘disturbance-like’ term or unknown system parameters in this scheme. The global stability of the closed-loop system can be proved.

We introduce a notion of reducibility of representations of topological spaces and study some basic properties of this notion for domain representations.

A representation reduces to another if its representing map factors through the other representation. Reductions form a pre-order on representations. A spectrum is a class of representations divided by the equivalence relation induced by reductions. We establish some basic properties of spectra, such as, non-triviality. Equivalent representations represent the same set of functions on the represented space.

Within a class of representations, a representation is universal if all representations in the class reduce to it. We show that notions of admissibility, considered both for domains and within Weihrauch's TTE, are universality concepts in the appropriate spectra. Viewing TTE representations as domain representations, the reduction notion here is a natural generalisation of the one from TTE.

To illustrate the framework, we consider some domain representations of real numbers and show that the usual interval domain representation, which is universal among dense representations, does not reduce to various Cantor domain representations. On the other hand, however, we show that a substructure of the interval domain more suitable for efficient computation of operations is equivalent to the usual interval domain with respect to reducibility.

We study isomorphisms of inductive types (that is, recursive types satisfying a condition of strict positivity) in an extensional simply typed $\lambda$-calculus with product and unit types. We first show that the calculus enjoys strong normalisation and confluence. Then we extend it with new conversion rules ensuring that all inductive representations of the product and unit types are isomorphic, and such that the extended reduction remains convergent. Finally, we define the notion of a faithful copy of an inductive type and a corresponding conversion relation that also preserves the good properties of the calculus.

Quantum physics, together with the experimental (and slightly controversial) quantum computing, induces a twist in our vision of computation, and hence, since computing and logic are intimately linked, in our approach to logic and foundations. In this paper, we discuss the most mistreated notion of logic, truth.

We propose a mathematical semantics for event-based architectures that serves two main purposes: to characterise the modularisation properties that result from the algebraic structures induced on systems by this discipline of coordination; and to further validate and extend the categorical approach to architectural modelling that we have been building around the language CommUnity with the ‘implicit invocation’, also known as ‘publish/subscribe’ architectural style. We then use this formalisation to bring together synchronous and asynchronous interactions within the same modelling approach. We see this effort as a first step towards a form of engineering of architectural styles. Our approach adopts transition systems extended with events as a mathematical model of implicit invocation, and a family of logics that support abstract levels of modelling.

It is well known that many real world networks have a power-law degree distribution (the scale-free property). However, there are no rigorous results for continuous-time quantum walks on such realistic graphs. In this paper, we analyse the space–time behaviour of continuous-time quantum walks and random walks on the threshold network model, which is a reasonable candidate model having the scale-free property. We show that the quantum walker exhibits localisation at the starting point, although the random walker tends to spread uniformly.

Quantum computation and quantum computational logics give rise to some non-standard probability spaces that are interesting from a formal point of view. In this framework, events represent quantum pieces of information (qubits, quregisters, mixtures of quregisters), while operations on events are identified with quantum logic gates (which correspond to dynamic reversible quantum processes). We investigate the notion of Shi–Aharonov quantum computational algebra. This structure plays the role for quantum computation that is played by σ-complete Boolean algebras in classical probability theory.

We show that the techniques for resource control that have been developed by the so-called light logics can be fruitfully applied also to process algebras. In particular, we present a restriction of higher-order π-calculus inspired by soft linear logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

In this paper, we are interested in high-level programming languages to implement the core components of an interactive theorem prover for a dependently typed language: the kernel – responsible for type-checking closed terms – and the elaborator – that manipulates open terms, that is terms containing unresolved unification variables.

In this paper, we confirm that λProlog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel. Indeed, we easily obtain a type checker for the Calculus of Inductive Constructions (CIC). Even more, we do so in an incremental way by escalating a checker for a pure type system to the full CIC.

We then turn our attention to the elaborator with the objective to obtain a simple implementation thanks to the features of the programming language. In particular, we want to use λProlog’s unification variables to model the object language ones. In this way, scope checking, carrying of assignments and occur checking are handled by the programming language.

We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to λProlog that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules.

We implement the proposed language extension in the Embedded Lambda Prolog Interpreter system and we discuss how it can be used to extend the kernel into an elaborator for CIC.