Search

International audience; In dependent type theory, impredicativity is a powerful logical principle that allows the definition of propositions that quantify over arbitrarily large types, potentially resulting in self-referential propositions. Impredicativity can provide a system with increased logical strength and flexibility, but in counterpart it comes with multiple incompatibility results. In particular, Abel and Coquand showed that adding definitional uniqueness of identity proofs (UIP) to the main proof assistants that support impredicative propositions (Coq and Lean) breaks the normalization procedure, and thus the type-checking algorithm. However, it was not known whether this stems from a fundamental incompatibility between UIP and impredicativity or if a more suitable algorithm could decide type-checking for a type theory that supports both. In this paper, we design a theory that handles both UIP and impredicativity by extending the recently introduced observational type theory TTobs with an impredicative universe of definitionally proof-irrelevant types, as initially proposed in the seminal work on observational equality of Altenkirch et al. We prove decidability of conversion for the resulting system, that we call CCobs , by harnessing proof-irrelevance to avoid computing with impredicative proof terms. Additionally, we prove normalization for CCobs in plain Martin-Löf type theory, thereby showing that adding proof-irrelevant impredicativity does not increase the computational content of the theory.

We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for ⋆-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo [Vincent Balat and Roberto Di Cosmo, 1999]. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek [Dominic Hughes and Rob van Glabbeek, 2005]. We then use the sequent calculus to extend our results to full MALL (including all units)., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 26:1-26:21

This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define a reference model of this structure as induced by a standard process calculus and we use this model to prove that parallel composition cannot be defined from the conjunctive structure alone., LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 28:1-28:21

International audience; We exhibit a strong connection between the matchgate formalism introduced by Valiant and the ZW-calculus of Coecke and Kissinger. This connection provides a natural compositional framework for matchgate theory as well as a direct combinatorial interpretation of the diagrams of ZW-calculus through the perfect matchings of their underlying graphs. We identify a precise fragment of ZW-calculus, the planar W-calculus, that we prove to be complete and universal for matchgates, that are linear maps satisfying the matchgate identities. Computing scalars of the planar W-calculus corresponds to counting perfect matchings of planar graphs, and so can be carried in polynomial time using the FKT algorithm, making the planar W-calculus an efficiently simulable fragment of the ZW-calculus, in a similar way that the Clifford fragment is for ZX-calculus. This work opens new directions for the investigation of the combinatorial properties of ZW-calculus as well as the study of perfect matching counting through compositional diagrammatical technics.

The set of pure terms which are typable in the $\lambda$$\Pi$-calculus in a given context is not recursive. So there is no general type inference algorithm for the programming language Elf and, in some cases, some type information has to be mentioned by the programmer.

Big data programming frameworks have become increasingly important for the development of applications for which performance and scalability are critical. In those complex frameworks, optimizing code by hand is hard and time-consuming, making automated optimization particularly necessary. In order to automate optimization, a prerequisite is to find suitable abstractions to represent programs; for instance, algebras based on monads or monoids to represent distributed data collections. Currently, however, such algebras do not represent recursive programs in a way which allows for analyzing or rewriting them. In this paper, we extend a monoid algebra with a fixpoint operator for representing recursion as a first class citizen and show how it enables new optimizations. Experiments with the Spark platform illustrate performance gains brought by these systematic optimizations., 36 pages

The problem of determining whether a term is an instance of another in the simply typed lambda -calculus, i.e. of solving the equation a=b where a and b are simply typed lambda -terms and b is ground, is addressed. An algorithm that decides whether a matching problem in which all the variables are at most third order has a solution is given. The main idea is that if the problem a=b has a solution, then it also has a solution whose depth is bounded by some integer s depending only on the problem a=b, so a simple enumeration of the substitutions whose depth is bounded by s gives a decision algorithm. This result can also be used to bound the depth of the search tree in Huet's semi-decision algorithm and thus to turn it into an always-terminating algorithm. The problems that occur in trying to generalize the proof given to higher-order matching are discussed. >

Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may require in particular to prove cut elimination for an extended notion of proof that combines deductions and computations. This suggests new interactions between automated theorem proving and proof theory.

International audience; Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the λ-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space used by the Space KAM, capturing into a type system the space complexity of the abstract machine. Additionally, we show how to capture also the time of the Space KAM, which is a reasonable time cost model, via minor changes to the type system.

International audience; The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.

Guarded tuple-generating dependencies (GTGDs) are a natural extension of description logics and referential constraints. It has long been known that queries over GTGDs can be answered by a variant of the chase ---a quintessential technique for reasoning with dependencies. However, there has been little work on concrete algorithms and even less on implementation. To address this gap, we revisit Datalog rewriting approaches to query answering, where GTGDs are transformed to a Datalog program that entails the same base facts on each base instance. We show that the rewriting can be seen as containing "shortcut" rules that circumvent certain chase steps, we present several algorithms that compute the rewriting by simulating specific types of chase steps, and we discuss important implementation issues. Finally, we show empirically that our techniques can process complex GTGDs derived from synthetic and real benchmarks and are thus suitable for practical use.

International audience; After observing that the truth conditions of connectives of non-classical logics are generally defined in terms of formulas of firstorder logic, we introduce 'protologics', a class of logics whose connectives are defined by arbitrary first-order formulas. Then, we introduce atomic and molecular logics, which are two subclasses of protologics that generalize our gaggle logics and which behave particularly well from a theoretical point of view. We also study and introduce a notion of equiexpressivity between two logics based on different classes of models. We prove that, according to that notion, every pure predicate logic with k ≥ 0 free variables and constants is as expressive as a predicate atomic logic, some sort of atomic logic. Then, we prove that the class of protologics is equally expressive as the class of molecular logics. That formally supports our claim that atomic and molecular logics are somehow 'universal'. Finally, we identify a subclass of molecular logics that we call predicate molecular logics and which constitutes its representative core: every molecular logic is as expressive as a predicate molecular logic. N.B.: This version of the paper corrects some typographical errors which are present in the published version, notably those regarding the references in Figures 2 and 3.

International audience; Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.

User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom’s decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, confluence of a terminating set of left-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. The present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pairs. The rewrite relation used for analyzing confluence may rewrite arbitrarily many non-overlapping redexes in a single step. This relation gives rise to critical pairs that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. Practical examples of use of this technique are analyzed.

International audience; The model checking problem for multi-agent systems against specifications in the alternating-time temporal logic AT L, hence AT L∗ , under perfect recall and imperfect information is known to be undecidable. To tackle this problem, in this paper we investigate a notion of bounded recall under incomplete information. We present a novel three-valued semantics for AT L∗ in this setting and analyse the corresponding model checking problem. We show that the three-valued semantics here introduced is an approximation of the classic two-valued semantics, then give a sound, albeit partial, algorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall. Finally, we extend MCMAS, an open-source model checker for AT L and other agent specifications, to incorporate bounded recall; we illustrate its use and present experimental results.

International audience; Sequential emulation is a semantics-based technique to automatically reduce property checking of distributed systems to the analysis of sequential programs. An automated procedure takes as input a formal specification of a distributed system, a property of interest and the structural operational semantics of the specification language and generates a sequential program whose execution traces emulate the possible evolutions of the considered system. The problem as to whether the property of interest holds for the system can then be expressed either as a reachability or as a termination query on the program. This allows to immediately adapt mature verification techniques developed for general-purpose languages to domain-specific languages, and to effortlessly integrate new techniques as soon as they become available. We test our approach on a selection of concurrent systems originated from different contexts from population protocols to models of flocking behaviour. By combining a comprehensive range of program verification techniques, from traditional symbolic execution to modern inductive-based methods such as property-directed reachability, we are able to draw consistent and correct verification verdicts for the considered systems.

International audience

The induction principle for natural numbers expresses that when a property holds for some natural number a and is hereditary, then it holds for all numbers greater than or equal to a. We present a similar principle for real numbers.

We give a new proof of a theorem of Mints that the positive fragment of minimal predicate logic is decidable. The idea of the proof is to replace the eigenvariable condition of sequent calculus by an appropriate scoping mechanism. The algorithm given by this proof seems to be more practical than that given by the original proof. A naive implementation is given at the end of the paper. Another contribution is to show that this result extends to a large class of theories, including simple type theory (higher-order logic) and second-order propositional logic. We obtain this way a new proof of the decidability of the inhabitation problem for positive types in system F.

A graph database is a digraph whose arcs are labeled with symbols from a fixed alphabet. A regular graph pattern (RGP) is a digraph whose edges are labeled with regular expressions over the alphabet. RGPs model navigational queries for graph databases called conjunctive regular path queries (CRPQs). A match of a CRPQ in the database is witnessed by a special navigational homomorphism of the corresponding RGP to the database. We study the complexity of deciding the existence of a homomorphism between two RGPs. Such homomorphisms model a strong type of containment between the two corresponding CRPQs. We show that this problem can be solved by an EXPTIME algorithm (while general query containmement in this context is EXPSPACE-complete). We also study the problem for restricted RGPs over a unary alphabet, that arise from some applications like XPath or SPARQL. For this case, homomorphism-based CRPQ containment is in NP. We prove that certain interesting cases are in fact polynomial-time solvable., 15 pages. Short version appeared in the proceedings of the 15th Conference on Computability in Europe (CIE 2019)

We extend the notion of Heyting algebra to a notion of truth values algebra and prove that a theory is consistent if and only if it has a B-valued model for some non trivial truth values algebra B. A theory that has a B-valued model for all truth values algebras B is said to be super-consistent. We prove that super-consistency is a model-theoretic sufficient condition for strong normalization.

Conway's field No of surreal numbers comes both with a natural total order and an additional "simplicity relation" which is also a partial order. Considering No as a doubly ordered structure for these two orderings, an isomorphic copy of No into itself is called a surreal substructure. It turns out that many natural subclasses of No are actually of this type. In this paper, we study various constructions that give rise to surreal substructures and analyze important examples in greater detail.

Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure λ-calculus, the process representations yield (at best) non-extensional λ-theories (i.e., β rule holds, whereas η does not). In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal π, Iπ (a subset of the π-calculus in which all outputs are bound), we develop a refinement of Milner's original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a λ-theory. Exploiting the symmetries and dualities of Iπ, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional λ-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite η. In contrast, the other two classes of wires yield nonextensional λ-theories whose equalities are those of the Lévy-Longo and Böhm trees.

The physical Church thesis is a thesis about nature that expresses that all that can be computed by a physical system-a machine-is computable in the sense of computability theory. At a first look, this thesis seems contradictory with the existence, in nature, of chaotic dynamical systems, that is systems whose evolution cannot be ''computed'' because of their sensitivity to initial conditions. The goal of this note is to show that there exist dynamical systems that are both computable and chaotic, and thus that the existence in nature of chaotic dynamical system is not, per se, a refutation of the physical Church thesis. Thus, chaos seems to be compatible with computability, in the same way as it is compatible with determinism.

We give a presentation of Simple Type Theory as a clausal rewrite system in Polarized deduction modulo.

We study two-player zero-sum turn-based games on graphs, a framework of choice in theoretical computer science. Such games model the possibly infinite interaction between a computer system (often called reactive) and its environment. The system, seen as a player, wants to guarantee a specification (translated to a game objective) based on the interaction; its environment is seen as an antagonistic opponent. The aim is to automatically synthesize a controller for the system that guarantees the specification no matter what happens in the environment, that is, a winning strategy in the derived game.A crucial question in this synthesis quest is the complexity of strategies: when winning strategies exist for a game objective, how simple can they be, and how complex must they be? A standard measure of strategy complexity is the amount of memory needed to implement winning strategies for a given game objective. In other words, how much information should be remembered about the past to make optimal decisions about the future? Proving the existence of bounds on memory requirements has historically had a significant impact. Such bounds were, for instance, used to show the decidability of monadic second-order theories, and they are at the core of state-of-the-art synthesis algorithms. Particularly relevant are the finite-memory-determined objectives (for which winning strategies can be implemented with finite memory), as they allow for implementable controllers. In this thesis, we seek to further the understanding of finite-memory determinacy. We divide our contributions into two axes.First, we introduce arena-independent finite-memory determinacy, describing the objectives for which a single automatic memory structure suffices to implement winning strategies in all games. We characterize this property through language-theoretic and algebraic properties of objectives in multiple contexts (games played on finite or infinite graphs). We show in particular that understanding the memory requirements in one-player game graphs (i.e., the simpler situation of games where the same player controls all the actions) usually leads to bounds on memory requirements in two-player zero-sum games. We also show that if we consider games played on infinite game graphs, the arena-independent-finite-memory-determined objectives are exactly the omega-regular objectives, providing a converse to the landmark result on finite-memory determinacy of omega-regular objectives. These results generalize previous works about the class of objectives requiring no memory to implement winning strategies.Second, we identify natural classes of objectives for which precise memory requirements are surprisingly not fully understood. We introduce regular objectives (a subclass of the omega-regular objectives), which are simple objectives derived from regular languages. We effectively characterize their memory requirements for each player, and we study the computational complexity of deciding the existence of a small memory structure. We then move a step up in the complexity of the objectives and consider objectives definable with deterministic Büchi automata. We characterize the ones for which the first player needs no memory to implement winning strategies (a property called half-positionality). Thanks to this characterization, we show that half-positionality is decidable in polynomial time for this class of objectives. These results complement seminal results about memory requirements of classes of omega-regular objectives.; Les jeux sur graphes à deux joueurs et à somme nulle constituent un modèle central en informatique théorique. De tels jeux modélisent une interaction potentiellement infinie entre un système dit réactif et son environnement. Le système est considéré comme un joueur et souhaite garantir une spécification (traduite en un objectif de jeu). Son environnement est considéré comme un joueur antagoniste. Le but est de synthétiser automatiquement un contrôleur pour le système qui garantit la spécification peu importe le comportement de l'environnement, ce qui correspond à construire une stratégie gagnante dans le jeu dérivé.Une question cruciale dans cette problématique de synthèse est celle de la complexité des stratégies : si des stratégies gagnantes existent, à quel point peuvent-elles être simples et à quel point doivent-elles être complexes ? Une mesure standard de complexité des stratégies est la quantité de mémoire nécessaire pour implémenter des stratégies gagnantes pour un objectif donné. En d'autres termes, quelle quantité d'information faut-il retenir au sujet du passé pour prendre des décisions optimales concernant le futur ? Des preuves de l'existence de bornes sur les besoins en mémoire ont historiquement eu un impact important. Par exemple, de telles bornes ont mené à des preuves de décidabilité de théories monadiques du second ordre, et sont au cœur de nombreux algorithmes efficaces pour la synthèse. Les objectifs déterminés à mémoire finie (c'est-à-dire ceux qui admettent des stratégies gagnantes se limitant à une mémoire finie) sont particulièrement pertinents, car ils mènent à l'existence de contrôleurs pouvant être implémentés en pratique. Dans cette thèse, nous cherchons à améliorer la compréhension de la détermination à mémoire finie. Nous distinguons deux axes dans nos contributions.Premièrement, nous introduisons le concept de détermination à mémoire finie indépendante de l'arène, qui décrit les objectifs pour lesquels une unique structure automatique de mémoire suffit pour implémenter des stratégies gagnantes dans tous les jeux. Nous caractérisons cette propriété via des propriétés algébriques et de langages dans différents contextes (jeux joués sur des graphes finis ou infinis). Nous montrons en particulier que la compréhension des besoins en mémoire dans les jeux à un joueur (c'est-à-dire les jeux plus simples dans lesquels le même joueur contrôle toutes les actions) mène généralement à des bornes sur les besoins en mémoire dans les jeux à deux joueurs et à somme nulle. Nous montrons également que si l'on considère les jeux joués sur des graphes infinis, les objectifs déterminés à mémoire finie indépendante de l'arène sont exactement les objectifs oméga-réguliers, ce qui fournit une réciproque au célèbre théorème de détermination à mémoire finie de ces objectifs. Ces résultats généralisent des travaux précédents au sujet des objectifs pour lesquels aucune mémoire n'est nécessaire pour les stratégies gagnantes.Deuxièmement, nous identifions des classes naturelles d'objectifs pour lesquels les besoins en mémoire ne sont pas complètement établis. Nous introduisons les objectifs réguliers (une sous-classe des oméga-réguliers), qui sont des objectifs dérivés de langages réguliers. Nous donnons une caractérisation effective des besoins en mémoire de ces objectifs pour chacun des joueurs, et nous étudions la complexité de décider de l'existence d'une petite structure de mémoire. Nous considérons ensuite des objectifs plus complexes définissables avec des automates de Büchi déterministes. Nous caractérisons ceux pour lesquels le premier joueur n'a besoin d'aucune mémoire pour implémenter des stratégies gagnantes (une propriété appelée semi-positionnalité). Grâce à cette caractérisation, nous montrons que la semi-positionnalité est décidable en temps polynomial pour ces objectifs. Ces résultats complètent des travaux fondateurs sur les besoins en mémoire des objectifs oméga-réguliers.

Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. Among the most successful ones, we can highlight type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own distance, and sensitivity analysis boils down to type checking. In particular, Fuzz features two product types, corresponding to two different notions of distance: the tensor product combines the distances of each component by adding them, while the with product takes their maximum.In this work, we show that these products can be generalized to arbitrary $$L^p$$ L p distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases $$L^1$$ L 1 and $$L^\infty $$ L ∞ . To ease the handling of such products, we extend the Fuzz type system with bunches—as in the logic of bunched implications—where the distances of different groups of variables can be combined using different $$L^p$$ L p distances. We show that our extension can be used to reason about quantitative properties of probabilistic programs.

In Rust, programs are often written using iterators, but these pose problems for verification: they are non-deterministic, infinite, and often higher-order, effectful and built using adapters. We present a general framework for specifying and reasoning with Rust iterators in first-order logic. Our approach is capable of addressing the challenges set out above, which we demonstrate by verifying real Rust iterators, including a higher-order, effectful . Using the Creusot verification platform, we evaluate our framework on clients of iterators, showing it leads to efficient verification of complex functional properties.

This paper introduces a robust class of functions from finite words to integers that we call Z-polyregular functions. We show that it admits natural characterizations in terms of logics, Z-rational expressions, Z-rational series and transducers. We then study two subclass membership problems. First, we show that the asymptotic growth rate of a function is computable, and corresponds to the minimal number of variables required to represent it using logical formulas. Second, we show that first-order definability of Z-polyregular functions is decidable. To show the latter, we introduce an original notion of residual transducer, and provide a semantic characterization based on aperiodicity., Comment: 27 pages

Instead of developing a customized typed lambda-calculus for each theory, we attempt to design a general parametric calculus that permits to express the proofs of any theory. This way, the problem of expressing proofs in the lambda-calculus is separated from that of choosing a theory.

In this note, we defend that the notion of algorithm as a set of execution traces is somewhat independent of the notion of abstract state machine. It can be reformulated in the more general framework of small step operational semantics.

Libraries of formal proofs are an important part of our mathematical heritage, but their usability and sustainability is poor. Indeed, each library is specific to a proof system, sometimes even to some version of this system. Thus, a library developed in one system cannot, in general, be used in another and when the system is no more maintained, the library may be lost. This impossibility of using a proof developed in one system in another has been noted for long and a remediation has been proposed: as we have empirical evidence that most of the formal proofs developed in one of these systems can also be developed in another, we can develop a standard language, in which these proofs can be translated, and then used in all systems supporting this standard. Logipedia is an attempt to build such a multi-system online encyclopedia of formal proofs expressed in such as standard language. It is based on two main ideas: the use of a logical framework and of reverse mathematics.

When a decision, such as the approval or denial of a bank loan, is delegated to a computer, an explanation of that decision ought to be given with it. This ethical need to explain the decisions leads to the search for a formal definition of the notion of explanation. This question meets older questions in logic regarding the explanatory nature of proof.

Graph data is omnipresent and has a wide variety of applications, such as in natural science, social networks, or the semantic web. However, while being rich in information, graphs are often noisy and incomplete. As a result, graph completion tasks, such as node classification or link prediction, have gained attention. On one hand, neural methods, such as graph neural networks, have proven to be robust tools for learning rich representations of noisy graphs. On the other hand, symbolic methods enable exact reasoning on graphs. We propose Knowledge Enhanced Graph Neural Networks (KeGNN), a neuro-symbolic framework for graph completion that combines both paradigms as it allows for the integration of prior knowledge into a graph neural network model. Essentially, KeGNN consists of a graph neural network as a base upon which knowledge enhancement layers are stacked with the goal of refining predictions with respect to prior knowledge. We instantiate KeGNN in conjunction with two state-of-the-art graph neural networks, Graph Convolutional Networks and Graph Attention Networks, and evaluate KeGNN on multiple benchmark datasets for node classification.

International audience; Due to the complexity and the magnitude of optimisation models that appeared in sustainable supply chain management (SSCM), the use of meta-heuristic algorithms as competent solution approaches is being increased in recent years. Although a massive number of publications exist around SSCM, no extant paper explicitly investigates the role of meta-heuristics in the sustainable (forward) supply chain. To fill this gap, a literature review is provided on meta-heuristic algorithms applied in SSCM by analyzing 160 rigorously selected papers published by the end of 2020. Our statistical analysis ascertains a considerable growth in the number of papers in recent years and reveals the contribution of 50 journals in forming the extant literature. The results also show that in the current literature the use of hybrid meta-heuristics is overtaking pure meta-heuristics, the genetic algorithm (GA) and the non-dominated sorting GA (NSGA-II) are the most-used single- and multi-objective algorithms, the aspects of sustainability are mostly addressed in connection with product distribution and routing of vehicles as pivotal operations in supply chain management, and last but not least, the economic-environmental category of sustainability has been further noticed by the scholars. Finally, a detailed discussion of findings and recommendations for future research are provided.

Researchers in neuroscience have a growing number of datasets available to study the brain, which is made possible by recent technological advances. Given the extent to which the brain has been studied, there is also available ontological knowledge encoding the current state of the art regarding its different areas, activation patterns, keywords associated with studies, etc. Furthermore, there is inherent uncertainty associated with brain scans arising from the mapping between voxels -3D pixels- and actual points in different individual brains. Unfortunately, there is currently no unifying framework for accessing such collections of rich heterogeneous data under uncertainty, making it necessary for researchers to rely on ad hoc tools. In this work we introduce NeuroLang, a probabilistic language based on first-order logic with existential rules, probabilistic uncertainty, ontologies integration under the open world assumption, and built-in mechanisms to guarantee tractable query answering over very large datasets. We propose that NeuroLang provides a substantial improvement to cognitive neuroscience research through the expressive power of its query language. We can leverage the ability of NeuroLang to seamlessly integrate useful heterogeneous data, such as ontologies and probabilistic brain atlases, to map fine-grained cognitive domains to brain regions through a set of formal criteria, promoting shareable and highly reproducible research on the domains of brain function. We believe that NeuroLang is well suited for leading computational approaches to formalize large-scale neuroscience research through probabilistic first-order logic programming.; Grâce aux récents progrès technologiques, le chercheur en neurosciences dispose d'une quantité croissante de jeux de données pour étudier le cerveau. La multiplicité des travaux dédiés a également produit des ontologies encodant des connaissances à la pointe concernant les différentes aires, les schémas d'activation, les mots-clés associés aux études, etc. Il existe d'autre part une incertitude inhérente aux images cérébrales, du fait de la mise en correspondance entre voxels - ou pixels 3D - et points réels sur le cerveau de différents sujets. Malheureusement, à ce jour, aucun cadre unifié ne permet l'accès à cette mine de données hétérogènes avec l'incertitude associée, obligeant le chercheur à se tourner vers des outils ad hoc. Dans cette étude, nous présentons NeuroLang, un langage probabiliste basé sur de la logique de premier ordre, comprenant des règles existentielles, de l'incertitude probabiliste, l'intégration d'ontologies reposant sur l'hypothèse du monde ouvert, ainsi que des mécanismes garantissant une réponse aux requêtes résolvables, même sur de très grandes bases de données. Nous soutenons que NeuroLang, par l'expressivité de son langage de requête, contribuera à grandement améliorer la recherche en neurosciences, en donnant notamment la possibilité d'intégrer de manière transparente des données hétérogènes, telles que des ontologies avec des atlas cérébraux probabilistes. Dans ce cas-ci, des domaines cognitifs - à la granularité fine - et des régions cérébrales seront associés via un ensemble de critères formels, favorisant ainsi la communication et la reproductibilité des résultats d'études sur les fonctions cérébrales. Aussi croyons-nous que NeuroLang est à même de se positionner en tête sur ces approches numériques qui visent à formaliser la recherche neuroscientifique à grande échelle via la programmation probabiliste et logique du premier ordre.

Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory. Our contribution is twofold: (i) We simplify this equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) We extend the complete equational theory to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings. The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.

Shortly before Larry Wos passed away, he sent a manuscript for discussion to Sophie Tourret, the editor of the AAR newsletter. We present excerpts from this final manuscript, put it in its historic context and explain its relevance for today’s research in automated reasoning.

Large-scale software verification relies critically on the use of compositional languages, semantic models, specifications, and verification techniques. Recent work on certified abstraction layers synthesizes game semantics, the refinement calculus, and algebraic effects to enable the composition of heterogeneous components into larger certified systems. However, in existing models of certified abstraction layers, compositionality is restricted by the lack of encapsulation of state. In this paper, we present a novel game model for certified abstraction layers where the semantics of layer interfaces and implementations are defined solely based on their observable behaviors. Our key idea is to leverage Reddy's pioneer work on modeling the semantics of imperative languages not as functions on global states but as objects with their observable behaviors. We show that a layer interface can be modeled as an object type (i.e., a layer signature) plus an object strategy. A layer implementation is then essentially a regular map, in the sense of Reddy, from an object with the underlay signature to that with the overlay signature. A layer implementation is certified when its composition with the underlay object strategy implements the overlay object strategy. We also describe an extension that allows for non-determinism in layer interfaces. After formulating layer implementations as regular maps between object spaces, we move to concurrency and design a notion of concurrent object space, where sequential traces may be identified modulo permutation of independent operations. We show how to express protected shared object concurrency, and a ticket lock implementation, in a simple model based on regular maps between concurrent object spaces.

Published in IFAC-PapersOnLine, 55(8):25-30, 2022; International audience; In 2010, the Research Center for Automatic Control (CRAN) proposed the concept of “communicating materials”, which led to this current project. Indeed, 3 French laboratories (the CRAN, LAAS and LIB) associated with one company (360SmartConnect/FINAO SAS) are working in the framework of the McBIM project to design a “communicating concrete”, made of concrete equipped with embedded low-energy wireless micro-sensors. This paper briefly describes the context of the McBIM project with the main research goal and objectives and then focus on the results in the different parts of the project regarding the different research issues, explored by the project.

We report on a new, simple, modular, and flexible approach for automated generation of illustrations for (readable) synthetic geometry proofs. The underlying proofs are generated using the Larus automated prover for coherent logic, and corresponding illustrations are generated in the GCLC language. Animated illustrations are also supported., Comment: In Proceedings ADG 2021, arXiv:2112.14770

SMPT (for Satisfiability Modulo Petri Net) is a model checker for reachability problems in Petri nets. It started as a portfolio of methods to experiment with symbolic model checking, and was designed to be easily extended. Some distinctive features are its ability to benefit from structural reductions and to generate verdict certificates. Our tool is quite mature and performed well compared to other state-of-the-art tools in the Model Checking Contest., FM 2023 - 25th International Symposium on Formal Methods,, Mar 2023, L{\"u}beck, Germany

Universal and complete graphical languages have been successfully designed for pure state quantum mechanics, corresponding to linear maps between Hilbert spaces, and mixed states quantum mechanics, corresponding to completely positive superoperators. In this paper, we go one step further and present a universal and complete graphical language for Hermiticity-preserving superoperators. Such a language opens the possibility of diagrammatic compositional investigations of antilinear transformations featured in various physical situations, such as the Choi-Jamio{\l}kowski isomorphism, spin-flip, or entanglement witnesses. Our construction relies on an extension of the ZW-calculus exhibiting a normal form for Hermitian matrices.

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic μMALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy μMALL validity criterion and how the language simulates the cut-elimination procedure of μMALL., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 13:1-13:18

Update: fixed an error on the applicability of thm 1, added some acks and a ref; We prove in constructive logic that the statement of the Cantor-Bernstein theorem implies excluded middle. This establishes that the Cantor-Bernstein theorem can only be proven assuming the full power of classical logic. The key ingredient is a theorem of Martín Escardó stating that quantification over a particular subset of the Cantor space ℕ → 2, the so-called one-point compactification of ℕ, preserves decidable predicates.

International audience; Cyclic induction is a powerful reasoning technique that can soundly stop the proof development and make the proof experience successful. In the setting of first-order logic with inductive definitions (FOLID), cyclic proofs can be built automatically by the Cyclist prover but their implementations are error-prone and the human validation may be tedious. On the other hand, cyclic induction is not yet integrated in certifying proof environments that support first-order logic and inductive definitions, as Isabelle and Coq.

International audience; We use the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative polarity, LJF proofs encode terms as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive polarity, LJF proofs yield a structure in which explicit sharing of term structures is possible. Such a representation of terms provides an explicit method for sharing term structures. In this setting, cut elimination yields a different notion of substitution. We illustrate these two approaches to term representation by applying them to the encoding of untyped λ-terms. We also exploit concurrency theory techniques-namely traces and simulation-to compare untyped λ-terms using such different structuring disciplines.