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.

We present a new model of guarded dependent type theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion and can therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves internally right orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one found in homotopy theoretic models of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann–Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.

N. G. de Bruijn, now professor emeritus of the Eindhoven University of Technology, was a pioneer in the field of interactive theorem proving. From 1967 to the end of the 1970's, his work on the Automath system introduced the architecture that is common to most of today's proof assistants, and much of the basic technology. But de Bruijn was a mathematician first and foremost, as evidenced by the many mathematical notions and results that bear his name, among them de Bruijn sequences, de Bruijn graphs, the de Bruijn–Newman constant, and the de Bruijn–Erdös theorem. The quotation above is thus interesting not because it is a reflection on his expertise in formal verification, but, rather, of his convictions as a working mathematician.

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.

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.

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.

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.

A Gentzen sequent calculus for Lax Logic is presented, the proofs in which correspond naturally in a 1–1 way to the normal natural deductions for the logic. The propositional fragment of this calculus is used as the basis for another calculus that uses a history mechanism in order to give a decision procedure for propositional Lax Logic.

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.

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.

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.

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.

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.

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.

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.

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.

We introduce infinitary propositional theories over a set and their models which are subsets of the set, and define a generalized geometric theory as an infinitary propositional theory of a special form. The main result is that the class of models of a generalized geometric theory is set-generated. Here, a class $\mathcal{X}$ of subsets of a set is set-generated if there exists a subset G of $\mathcal{X}$ such that for each α ∈ $\mathcal{X}$, and finitely enumerable subset τ of α there exists a subset β ∈ G such that τ ⊆ β ⊆ α. We show the main result in the constructive Zermelo–Fraenkel set theory (CZF) with an additional axiom, called the set generation axiom which is derivable in CZF, both from the relativized dependent choice scheme and from a regular extension axiom. We give some applications of the main result to algebra, topology and formal topology.