The date for the annunal meeting WG 1.6 is Saturday, September 9, 2017. The WG 1.6 is part of FSCD and will take place one day after the main conference.
Abstract: In this talk, I will present recent work on automatic analysis of concurrent message-passing systems, modelled by the pi-calculus. In the course of a computation, such a system generates an unbounded set of processes (and of names), with a dynamically evolving communication topology. We are interested in the shape invariants satisfied by the communication topology, and the automatic inference of these invariants. We introduce the concept of "hierarchical" system, which is a pi-term whose communication topology is shaped by a finite forest T, specifying the hierarchical relationship between names. I will discuss the design of a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of pi-calculus reactions. The coverability problem for hierarchical terms is decidable, which is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the pi-calculus with decidable safety verification problems. Time permitting, we will briefly discuss an application of such resource-bounded systems to the automatic verification of secrecy in the analysis of cryptographic protocols. (This is based on joint work with Emanuele D'Osualdo.)
Abstract: Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. However, in existing programming and proof environments this can be costly and time consuming, as we need to repeatedly build up low-level infrastructure from scratch and using it in formal developments is tedious and error prone. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga relies on the logical framework LF; to reason about formal systems, Beluga provides a dependently typed functional language for implementing (co)inductive proofs about derivation trees as (co)recursive functions following the Curry-Howard isomorphism. Key to this approach is the ability to model derivation trees that depend on a context of assumptions using a generalization of the logical framework LF, i.e. contextual LF which supports first-class contexts and simultaneous substitutions. Our experience demonstrates that Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics.
Abstract: Confluence for terminating systems are decidable from the well-known result by Knuth and Bendix; it coincides with the joinability of critical pairs. We, however, have few studies on confluence (not innermost confluence) for innermost terminating systems. This talk introduces a short history on confluence of innermost terminating systems, and then shows that it is characterized by innermost joinability of all normal instances of the critical pairs. By using this characterization, we give two decidable sufficient conditions.
Abstract: We present work-in-progress on the generalisation from first-order to higher-order term rewriting, of Okui's 1998 theorem stating that a left-linear term rewrite system is confluent if all its multi--one critical peaks are many--multi joinable. As the proof became very lengthy, we found a need to revisit and integrate basic notions and results in first-order term rewriting. In particular, we developed alternative perspectives on first-order rewriting (by second-order means), critical pairs (using a lattice-theoretic formulation), and Huet's critical pair lemma and Rosen's confluence-by-ortogonality theorem (integrating them and their proofs via re/decomposition). The talk is essentially a request for comments on these alternative perspectives.
The meetings of the working group are public, with the single exception of the business meeting.