You may also be interested by the page where I collected not easily accessible publications by several authors in the domain of term rewriting and type theory.
See also the support of talks I gave.
The following list is not exhaustive. For a more complete list see the list of my publications (or DBLP which gives a less up-to-date list).
A new presentation of Conversion/Preference Games updating JAIST/IS-RR-2006-006.
In this tutorial we introduce the concept of CP-game which is a generalization of this of strategic game. First we present examples which are relevant to a CP-game approach. Then we give a somewhat naive introduction to CP-games. Then we present the connection between CP games and gene regulation networks as presented by Rene Thomas.
This paper introduces a framework based on game theory that models gene regulation activities. The games used here are called Conversion/Preference games or CP Games in short. CP game theory is a discrete presenetation of game theory that extends nicely classical strategic game theory. A group of genes is a module if a connection between the regulation activity of that group of genes and some biological functions can be established. One of the main issue when a gene regulation system is analyzed through a model is to decompose the model into modules. Assuming that a gene regulation system can be decomposed into modules and that each module "implements" a function, the goal of dynamical analysis is to exhibit the module structure. More specifically we focus on regulation equilibria that give a stable answer to stress One of the key issue in order to identify modules is the ability to decompose the system into games. the analysis of the dynamics of games, enable to understand how new equilibria may emerge in the composed game. In this paper we give partial answers to these questions.
We present a game-theoretic foundation for gene regulatory analysis based on the recent formalism of rewriting game theory. Rewriting game theory is discrete and comes with a graph-based framework for understanding compromises and interactions between players and for computing Nash equilibria. The formalism explicitly captures the dynamics of its Nash equilibria and, therefore, is a suitable foundation for the study of steady states in discrete modelling. We apply the formalism to the discrete analysis of gene regulatory networks introduced by R. Thomas and S. Kaufman. Specifically, we show that their models are specific instances of a C/P game deduced from the K parameter.
Finite objects and more specifically finite games are formalized using induction, whereas infinite objects are formalized using coinduction. In this article, after an introduction to the concept of coinduction, we revisit on infinite (discrete) extensive games the basic notions of game theory. Among others, we introduce a definition of Nash equilibrium and a notion of subgame perfect equilibrium for infinite games. We use those concepts to analyze well known infinite games, like the dollar auction game and the centipede game and we show that human behaviors that are often considered as illogic are perfectly rational, if one admits that human agents reason coinductively.
This paper has been rejected by the International
Journal of Game Theory and the report
is worth reading.
In this paper we study carefully and formally the dollar auction game using coinduction and we show that unlike what is commonly admitted the behavior which consists in bidding forever and which is called escalation is rational. Escalation is typical of an infinite game and tools conceived for studying infiniteness are mandatory and they are what coinduction provides.
This paper has been rejected by the journal Games and Economic Behavior and the report is a piece of anthology of what can be written by somone who knows nothing about coinduction and computability. Here is my answer.
This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the eponymous modality that says that a group of agents shares a knowledge about a certain proposition in a inductive way. This modality is specified by using a fixpoint approach. Furthermore, from these experiments, we discuss and compare the structure of theorems that can be proved in specific theories that use common knowledge logic. Those structures manifests the interplay between the theory (as implemented in the proof assistant Coq) and the metatheory.
Common Knowledge Logic is meant to describe situations of the real world where a group of agents is involved. These agents share knowledge and make strong statements on the knowledge of the other agents (the so called common knowledge). But as we know, the real world changes and overall information on what is known about the world changes as well. The changes are described by dynamic logic. To describe knowledge changes, dynamic logic should be combined with logic of common knowledge. In this paper we describe experiments which we have made about the integration in a unique framework of common knowledge logic and dynamic logic in the proof assistant Coq. This results in a set of fully checked proofs for readable statements. We describe the framework and how a proof can be conducted.
This paper proposes a formalization in Coq of common knowledge logic and checks its adequacy on case studies. This exercise allows exploring experimentally the proof-theoretic side of common knowledge logic. This work is original in that nobody has considered higher order common knowledge logic from the point of view of proofs performed on a proof assistant. This work is experimental by nature as it tries to draw conclusions from experiments with a proof assistant.
We develop an intersection type system for the lambda-mu-mu~ calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves on earlier type disciplines for lambda-mu-mu~: in addition to characterizing the lambda-mu-mu~ expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.
*X is a diagrammatic calculus. This means that it describes programs by 2-dimensional diagrams and computations are reductions of those diagrams. In addition it has a 1-dimensional syntax. Type system of *X interprets simply classical logic in a Curry-Howard correspondence. Since lambda-calculus can be easily implemented, its untyped version is Turing complete.
We investigate some syntactic properties of Wadler's dual calculus, a term calculus which corresponds to classical sequent logic in the same way that Parigot's lambda-µ calculus corresponds to classical natural deduction. Our main result is strong normalization theorem for reduction in the dual calculus; we also prove some confluence results for the typed and untyped versions of the system.
X is an untyped language for describing circuits by composition of basic components. This language is well suited to describe structures which we call "circuits" and which are made of parts that are connected by wires. Moreover X gives an expressive platform on which algebraic objects and many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for X and some its potential uses. To demonstrate the expressive power of X, we will show how, even in an untyped setting, elaborate calculi can be embedded, like the naturals, the lambda-calculus, Bloe and Rose's calculus of explicit substitutions lambda-x, Parigot's lambda-mu and Curien and Herbelin's lambda-mu-mu~.
We investigate some fundamental properties of the reduction relation in the untyped term calculus derived from Curien and Herbelin's lambda-mu-mu~. The original lambda-mu-mu~ has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic; the significance of the untyped calculus of raw terms is that it is a Turing-complete language for computation with explicit representation of control as well as code. We define a type assignment system for the raw terms satisfying: a term is typable if and only if it is strongly normalizing. The intrinsic symmetry in the lambda-mu-mu~ calculus leads to an essential use of both intersection and union types; in contrast to other union-types systems in the literature, our system enjoys the Subject Reduction property.
We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are strongly normalizing. This system extends previous work on the natural generalization of the classical intersection types system, which characterized head normalization and weak normalization, but was not complete for strong normalization. An important role is played by the notion of available variable in a term, which is a generalization of the classical notion of free variable.
We characterize those terms which are strongly normalizing in a composition-free calculus of explicit substitutions by defining a suitable type system using intersection types. The key idea is the notion of available variable in a term, which is a generalization of the classical notion of free variable.
This paper is part of a general program of treating explicit substitutions as the primary lambda-calculi from the point of view of foundations as well as applications. We work in the composition-free calculus lambda-x of explicit substitutions and the augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction. We show that the strongly normalizable terms, the terms which normalize by leftmost reduction, and the terms which normalize by head reduction can each be characterized as the terms typable in a certain system. As a consequence we characterize a class of deterministic reduction strategies which are normalizing strategies and so can serve as models for evaluation in functional programming. The type systems we study are the natural generalizations of the classical systems, but the proofs require some new techniques in the presence of explicit reductions involving substitutions. Indeed, in our proofs we do not rely on results from classical lambda-calculus, which in our view comes after the calculus of explicit substitution. The proof technique we employ yields readily the result that a term is strongly normalizing iff it is strongly normalizing in the calculus extended by garbage-collection.
This short note presents a calculus of explicit substitutions proposed by N. G. de Bruijn in 1978.
Explicit substitutions were proposed by Abadi, Cardelli, Curien, Hardin and Lévy to internalise substitutions into lambda-calculus and to propose a mechanism for computing on substitutions. lambda-upsilon is another view of the same concept which aims to explain the process of substitution and to decompose it in small steps. lambda-upsilon is simple and preserves strong normalisation. Apparently that important property cannot stay with another important one, namely confluence on open terms. The spirit of lambda-upsilon is closely related to another calculus of explicit substitutions proposed by de Bruijn and called C-lambda-xi-phi. In this paper, we introduce lambda-upsilon, we present C-lambda-xi-phi in the same framework as lambda-upsilon and we compare both calculi. Moreover, we prove properties of lambda-upsilon; namely lambda-upsilon correctly implements beta reduction, lambda-upsilon is confluent on closed terms, i.e., on terms of classical lambda-calculus and on all terms that are derived from those terms, and finally lambda-upsilon preserves strong normalization of beta-reduction.
Lambda-upsilon calculus is a new simple calculus of explicit substitutions. In this paper we explore its properties, namely we prove that it correctly implements beta-reduction, it is confluent, its simply typed version is strongly normalizing. We associate with lambda-upsilon an abstract machine called the U-machine and we prove that the U-machine correctly implements lambda-upsilon.
This paper published in POPL'94 gives a systematic description of several calculi of explicit substitutions. These systems are orthogonal and have easy proofs of termination of their substitution calculus. The last system, called lambda-upsilon, entails a very simple environment machine for strong normalization of lambda-terms.
We describe the foundations of Obj-a, a framework, or generic calculus, for modeling object-oriented programming languages. This framework provides a setting for a formal operational semantics of object based languages, in the style of the Lambda Calculus of Objects of Fisher, Honsell, and Mitchell. As a formalism for specification, Obj-a is arranged in modules, permitting a natural classification of many object-based calculi according to their features. In particular, there are modules for calculi of non-mutable objects (i.e., functional object-calculi) and for calculi of mutable objects (i.e., imperative object-calculi). As a computational formalism, Obj-a is based on rewriting rules. However, classical first-order term rewriting systems are not appropriate to reflect aspects of implementation practice such as sharing, cycles in data structures and mutation. Therefore, the notion of addressed terms and the corresponding notion of addressed term rewriting are developed.
A version slightly revised and shortened has been published at FM'99. World Congress on Formal Methods (FM'99) 20-24 September 1999, Toulouse, France , Springer LNCS vol. 1709, pp. {963-982}
A proof of well-foundedness of the recursive path ordering based on simple principles.
This paper studies three orderings, useful in theorem proving, especially for proving termination of term rewriting systems: the recursive decomposition ordering with status, the recursive path ordering with status and the closure ordering. It proves the transitivity of the recursive path ordering, the strict inclusion of the recursive path ordering in the recursive decomposition ordering, the totality of the recursive path ordering -- therefore of the recursive decomposition ordering --, the strict inclusion of the recursive decomposition ordering in the closure ordering and the stability of the closure ordering by instantiation.
The ability to use a polynomial iterpretation to prove termination of a rewrite system naturally prompts the question as to what restriction on complexity this imposes. The main result of this paper is that a polynomial interpretation termination proof of a rewrite system which computes a number theoretic function implies a polynomial bound on that function's rate of growth.
This paper presents the first version of the recursive decomposition ordering with status.
Note: The version presented at the conference, which is the one given here, had a slightly different title namely Uniform Termination of Term Rewriting Systems: an new Recursive Decomposition Ordering and its Implementation from the one published in the final proceedings.
In this paper that appeared in Theoretical Computer Science vol. 132, (1994), pp (395-401) we reduce the problem of termination of one rule rewrite systems to problems somewhat more related to rewrite systems namely to Post correspondence problems and to termination of semi-Thue systems. Proofs we obtain this way are shorter and we expect other interesting applications from these codings. In particular, the second part proposes a simulation of semi-Thue systems by one rule systems.
Inductive theorems are properties valid in the initial algebra. A now popular tool for proving them in equational theories or abstract data types is based on proof by consistency. This method uses a completion procedure and requires two essential properties of the specification, namely relative completeness and omega-completeness. This paper investigates ways of proving them. For the first one, the complement algorithm is presented. It is based on unification and computation of coverings and complements. For the second one, a technique based on discrimination of pairs of normal forms is explained and illustrated through examples.
The identities which are stable for power extensions of heterogeneous algebras are characterized by linearity and regularity properties. These results are use to study nondeterministic models of abstract data types and identities they satisfy. They constitute an adequate framework for the study of algebraic sets in heterogeneous algebras.
Ceci est un ensemble de notes que j'ai écrites en 1972 pour mes collègues de Nancy quand j'ai été fasciné par le lambda-calcul et le modèle de Scott. En fait, je n'ai retravaillé sur le lambda-calcul qu'en 1993 quand j'ai été fasciné par les substitutions explicites.
Ceci est un livre publié en 1978 dont j'ai été le co-auteur.
In this paper we show that a limited vocabulary can lead to strange and irregular situations. A complete analysis is given using five simple canonical case studies.
This talk has been given as the banquet speech at the 3rd UNIF 1989
This text in French teases the kind of research done in France at that time(1, 2, 3).