-------------------------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: June 26, 2019 (Dortmund, Germany) Chair: Georg Moser Secretary: Martin Avanzini -------------------------------------------------------------------------------- PARTICIPANTS Beniamino Accatolli Cynthia Kop (invited) Daniel Dougherty Delia Kesner Hans Zantema Herman Geuvers (report FSCD) Juergen Giesl Luigi Liquori Manfred Schmidt-Schauß Martin Avanzini Masahiko Sakai Narciso Marti-Oliet (report ISR) Ralf Treinen Rene Thiemann (invited) Silvia Ghilezan (invited) Takahito Aoto -------------------------------------------------------------------------------- AGENDA 1) Presentation by Cynthia Kop (invited) 2) Presentation by Rene Thiemann (invited) 3) Report on FSCD by Herman Geuvers 4) Report on IFIP by Martin Avanzini 5) Presentation by Silvia Ghilezan (invited) 5) Report on ISR by Hans Zantema (invited) 6) Business Meeting -------------------------------------------------------------------------------- 1) Presentation by Cynthia Kop. Title: Cons-free rewriting Abstract: The area of implicit complexity aims to study complexity classes (such as P, NP, LOGSPACE, ...) by encoding queries into calculi or logics. One such approach, introduced by Jones in 2001, is to use read-only ("cons-free") functional programs with restrictions on type orders. In this talk, I describe this work, and discuss the (significant!) effects of using term rewriting systems instead of functional programs. 2) Presentation by Rene Thiemann. Improved Certification of Complexity Proofs for Term Rewrite Systems Abstract: Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of A^n for a fixed non-negative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations. We present a new variant of the Perron-Frobenius theorem in order to completely avoid algebraic numbers computations that have previously been necessary when certifying complexity proofs. To formalize the theorem in Isabelle/HOL, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. 3) Report on FSCD by Herman Geuvers Herman Geuvers gave a brief report on FSCD with a particular focus of the role of the rewriting community on FSCD. - Rewriting community was sufficiently represented in the PC and provided clear/sufficient input - 69 papers were submitted - 12 papers fell clearly in the context of rewriting, out of which 6 were accepted. - 12 lambda-calculus/explicit substitution paeprs were submitted, 7 accepted - The experience with LIPIcs was good. - An LMCS special issue is planned, Femke van Raamsdonk will be co-editor. - Four invited speakers were selected, with an emphasis on diversity (gender / region / topic). 4) Report on IFIP by Martin Avanzini Martin Avanzini gave a brief report on IFIP TC1. - Luis Suares Barbosa ( http://www4.di.uminho.pt/~lsb/ ) is new chair of TC1. - A TC1 (virtual) meeting took place on the 14/06/19 with IFIP WG1 chairs & representatives of nations. - IFIP WG 1.6 chair Georg Moser could not join the video conference, due to technical reasons. - Georg Moser requested a protocol well in advance of the IFIP WG1.6 meeting, but received no answer to date. - It is intended to schedule annual TC1 face-to-face meetings collocated with major event. Most decisions will be made asynchronously, via the mailing list. Video conferences are planned for small meetings, if required. - It is not desired to collocate the annual IFIP WG 1.6 meeting with the TC1 meeting. 5) Presentation by Silvia Ghilezan (invited) Title: Denotational and Operational Preciseness of Subtyping Abstract: The notion of subtyping has gained an important role in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different aspects: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed for iso-recursive types with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. We present a technique for formalising and proving operational preciseness of the subtyping relation in concurrent lambda calculus with intersection and union types. An overview of preciseness of subtyping in the setting of session and multiparty session type will be given. We then discuss a universal (language independent) framework to reason about preciseness of subtyping. (The talk is based on the results obtained jointly with Mariangiola Dezani-Ciancaglini, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas and Nobuko Yoshida.) 5) Report on ISR by Hans Zantema (invited) Hans Zantema read the report on the successful ISR 2018 written by Camilo Rocha. Hans Zantema gave a brief report on ISR 2019. - ISR is searching for candidate locations for ISR 2021/2022. Candidates from Japan and USA are particularly encouraged, as no past ISR was held in these countries. Narciso Marti-Oliet gave a brief status report on the organisation of the upcoming ISR at UCM Madrid. - Speakers will be selected by invitation and via an open call. - It is envisioned that the school takes place in the second two weeks of July 2020. The precise dates depend on the availability of cheap student accommodations on campus and will be decided later. - Registration fees will be in the range of 300-350Euro. Accommodation will cost around 35Euro per day. - Luigi Liquori proposed to make the lectures available to a broad audience via streaming, MOOC or similar technologies. The idea was considered favourable by the participants of the meeting. 6) Business Meeting - No problems with current memberships have been found. - The three invited speakers (Silvia Ghilezan, Cynthia Kop, Rene Thiemann) have been voted unanimous to join IFIP WG 1.6 via an open vote. - It has been decided that the next IFIP WG 1.6 meeting should take place collocated with FSCD in Paris 13. Precise dates will be decided later via the mailing list. - While the workshops program has been distributed in advance via the IFIP WG 1.6 mailing list, it was available online only at he day of the meeting. Since the meeting is open to the public (except for the business meeting) it is desirable to have the program available online well in advance. This should be taken care of by the chair and secretary in future iterations. - The chairs (second and thus final) term will end in 2020. Chair and secretary are advised to approach candidates for the next term. To relief working effort of the chair, a vice-chair could be appointed even earlier, as permitted by the by-laws.