Search

Residuals of redexes keep track of redexes along reductions in the lambda calculus. Families of redexes keep track of redexes created along these reductions. In this paper, we review these notions and their relation to a labeled-calculus introduced here in a systematic way. These properties may be extended to combinatory logic, term rewriting systems, process calculi and proofnets of linear logic.

Quite often formal proofs are not published in conferences or journal articles, because formal proofs are usually too long. A typical article states the ability of having implemented a formal proof, but the proof itself is often sketched in terms of a natural language. At best, some formal lemmas and definitions are stated. Can we do better ? We try here to publish the details of a formal proof of the white-paths theorem about depth-first search in graphs. We use Why3 as the proving platform, because Why3 uses first-order logic augmented with inductive definitions of predicates and because Why3 makes possible to delegate bits of proofs to on-the-shelf automatic provers at same time as Why3 provides interfaces with interactive proof checkers such that Coq, PVS or Isabelle. Algorithms on graphs are also a good testbed since graphs are combinatorial structures whose algebraic properties are not fully obvious. Depth-first search may look over-simple, but it is the first step of the construction of a library of readable formal proofs for more complex algorithms on graphs with more realistic data structures.

Travail présenté à JFLA 2017; National audience; Nous présentons une preuve formelle de l'algorithme de Tarjan (1972) pour trouver les composantes fortement connexes dans un graphe. Cet algorithme exécute une seule passe sur le graphe le parcourant en profondeur d'abord. Notre programme est ici écrit dans un style de programmation fonctionnelle dans le langage Why3-ML. La preuve utilise des lemmes et des assertions exprimés dans la logique de Why3. La majorité d'entre eux sont prouvés automatiquement à l'exception de 5 assertions ou lemmes prouvés manuellement en Coq. Une preuve d'une version impérative de ce programme ne figure pas dans ce travail, mais nous indiquons comment y parvenir par raffinements successifs. Un point important est que nos preuves sont intuitives, publiables et lisibles par un humain.

We present formal proofs for the two classical Tarjan-1972 and Kosaraju-1978 algorithms for finding strongly connected components in directed graphs. We describe the two algorithms in a functional programming style with abstract values for vertices in graphs, with functions between vertices and their successors, and with data types such that lists (for representing immutable stacks) and sets. We use the Why3 system and the Why3-logic to express these proofs and fully check them by computer. The Why3-logic is a simple multi-sorted first-order logic augmented by inductively defined predicates. Furthermore it provides useful libraries for lists and sets. The Why3 system allows description of programs in a Why3-ML programming language (a first-order programming language with ML syntax) and provides interfaces to various state-of-the-art automatic provers and to manual interactive proof-checkers (we use mainly Coq). One important point of our article is that our proofs are intuitive and human readable.

Projet CHLOE, Projet PARA; Categorical combinators and more recently ls-calculus have been introduced to provide an explicit treatments of substitutions in the l-calculus. We reintroduce here the ingredients of these calculi in a self-contained and stepwise way, with a special emphasis on confluence properties. The main new results of the paper w.r.t. are the following : - we present a confluent weak calculus of substitutions, where no variable clashes can be feared - we solve a conjecture : ls-calculus is not confluent (it is confluent on ground terms only). This unfortunate result is "repaired" by presenting a confluent version of ls-calculus, named the lEnv-calculus called here the confluent ls-calculus.

Disponible dans les fichiers attachés à ce document

IntroductionBohm's theorem: applications to Computer Science Theory - BOTH 2001This part of the volume contains the Proceedings of the ICALP 2001 Satellite Workshop on Bohm's theorem: applications to Computer Science Theory (BOTH 2001), held in the Aldemar Knossos Royal Village Hotel, Hersonissos, Crete, Greece on 13 July 2001.Bohm's theorem is central to the study of the untyped lambda calculus. It shows that disctinct normal forms, up to eta conversion, cannot be identified in any consistent model of the lambda calculus. This first separability result has been generalised to non normal forms and is the underlying concept for the introduction of finite or infinite trees of head normal forms, also known as Bohm trees.In the semantics of programming languages, Bohm's theorem corresponds to the notion of full abstraction in models, and gave the initial hints towards the construction of models for sequential languages; in the theory of concurrency, it is the notion of observability and is used for building bisimulations; in the semantics of security, it gives a strong meaning to the notion of safe computations.Thirty years later, on the occasion of Corrado Bohm's EATCS Distinguished Service Award, this workshop attempted to provide a synthetic view as well as the most recent results on Bohm trees, sequentiality and game semantics, logic, security, fully abstract translations, action calculi, abstract rewriting systems, based on the seminal work of Bohm.BOTH 2001 was one of the four satellite workshops of the 28th International Colloquium on Automata, Languages and Programming (ICALP 2001), held in Crete, Greece, July 8-12, 2001.The proceedings appear as Volume 50 No. 2 in the series Electronic Notes in Theoretical Computer Science (ENTCS). The volumes in the ENTCS series can be accessed at the URL http://www.elsevier.nl/locate/entcs.The Program Committee selected five contributions by researchers from several different countries: France, Italy, Japan, Yugoslavia. Selected contributions are connected to Bohm's theorem or Bohm's research. The program included also two invited talks by Henk Barendregt (Univ. of Nijmegen) and Mariangiola Dezani (Univ. di Torino). Pierre-Louis Curien also offered to give a talk on Separation in Girard's Ludical framework.The program committee of BOTH 2001 consisted of the following people: •Pierre-Louis Curien (CNRS, Univ. of Paris 7)•Gérard Huet (INRIA, France)•Jan-Willem Klop (Free University, Amsterdam)•Jean-Jacques Lévy (INRIA, France)•Harry Mairson (Boston University)•Gordon Plotkin (Univ. of Edinburgh)•Simona Ronchi (Univ. of Torino)We would like to thank Christos Zaroliagis (ICALP 2001 Satellite Workshops Coordinator) for his continuous support.July 2001 Jean-Jacques Lévy