MINUTES OF THE IFIP WORKING GROUP (9/9/2017, OXFORD, UK)

9:30: The meeting starts.

9:30: Dale Miller, report on FSCD.
He reports on acceptance ratio, submissions, statistics, LIPIcs.
Questions: Brigitte Pientka proposed a co-location with ICFP. Helene Kirchner questioned about the necessity (or not) for FSCD to go with other conferences. Georg Moser asked Miller whether a three-day conference is to be preferred to a four-day one.  Some discussion about system descriptions and award to young students. Fernandez proposed to have more awards. Moser proposed to have a Test of Time Award. Some general consensus arises as to have a more “permissive” Junior Award. System descriptions are very hard to evaluate, as most audience agree. It cannot be just the description of a technique, nor the description of the (best) tool for a problem. A little discussion about artifact evaluation. Another proposal: have a special committee for tool submission. Ong updates about FSCD 2020, which will be in in Paris, a venue with large potential capacity. Colocation with CADE or IJCAR? Brigitte asked about having FSCD outside of Europe? Ong replied that in 2021 it could be done in Buenos Aires. 

10:30: Vincent van Oostrom, technical talk. 
TITLE: Critical Pairs Redefined (joint work with Hirokawa, Nagele, Oyamaguchi).
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.

11:30: Luke Ong, technical talk 
TITLE: On Hierarchical Communication Topologies of Concurrent Message-passing Systems
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.

12:15: Johannes Waldmann. Report on ISR school.
Questions: the audience asked about how courses are selected. Waldmann replied that it’s always a problem to find a good set of speakers and courses. The audience asked about potential conflicts between ISR 2018 and FLOC. Waldmann replied the they were discovered too late.

12:30: Olivier Hermant. Proposal to host ISR 2019 in Paris.
Questions: Moser would like the idea of having everybody at the same accommodation. Waldmann asked how many slots should an advanced course take.
VOTE on Olivier proposals: favour (9, everybody)

14:00 Brigitte Pientka, technical talk.
TITLE: Mechanizing Meta-Theory in Beluga.
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.

14:45 Masahiko Sakai, technical talk.
TITLE  On Confluence of Innermost Terminating Term Rewriting Systems.
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.

16.00 Business Meeting. (Hirokawa, Moser, Middledorp, Kirchner, Van Oostrom, Dal Lago)