July 24, 2021 - Buenos Aires, Argentina (virtualised)

Date

The date for the annunal meeting of the IFIP WG 1.6 is Saturday, July 24, 2021. The meeting is part of (virtualised) FSCD 2021 and will take place as post-conference workshop.

Aims

To support the development of rewriting in particular and the study of formal structures in computations and deductions in general.
To expand on the awareness and success of rewriting and lambda calculus in theoretical computer science.
Represent and seek cooperations between all communities working on formal structures in computations and deductions.
To foster development of applications of theoretical advances.

Invited Speakers

Mauricio Ayala-Rincón
Formalization of the Termination of Functional Specifications in PVS
Abstract: This talk will present research on the formalization of automation of the termination for a functional language model called PVS0 designed for the meta-theoretical study of the PVS higher-order logic and its computational aspects. The PVS0 model is validated by proving its fundamental computability properties. Termination criteria related to PVS type-correctness conditions, size-change principle, calling-context and matrix-weighted graphs, and dependency pairs are specified. The correction of such termination criteria is guaranteed by formalizing their equivalence.
Jörg Endrullis
Graph Rewriting
Abstract: There are various graph rewriting approaches based in category theory, for instance the well-known Double Pushout approach (DPO). We discuss some shortcomings of the existing frameworks, in particular concerning relabeling and control over the embedding in the context. We introduce a novel framework PBPO+ that overcomes these limitations.
Sarah Winkler
Decidable Fragments of First-order Logic via Termination of Rewriting
Abstract: This talk presents new fragments of first-order logic whose decidability with respect to resolution techniques and the SGGS method is witnessed by existence of a suitable ordering on atoms. These fragments include the restrained, the sort-restrained, and the controlled class. Membership of a clause set in these classes can be tested by extracting a first-order term rewrite system from the clauses and proving it terminating with respect to rewriting or narrowing, using state-of-the-art automatic termination tools. The talk is partially based on the following paper: M.P. Bonacina and S. Winkler: SGGS Decision Procedures. In Proc. 10th IJCAR, volume 12166 of LNCS, pages 356-374, 2020. http://dx.doi.org/10.1007/978-3-030-51074-9_20

Preliminary Program

    06:30 - 07:30: Session 1
    - 60' presentation Mauricio Ayala-Rincón    

    07:30 - 08:00: Break

    08:00 - 10:00: Session 2
    - 60' presentation Jörg Endrullis
    - 60' presentation Sarah Winkler

    10:00 - 10:30: Break

    10:30 - 12:30: Session 3
    - 15' report   ISR 2021 (Madrid) by Narciso Martí Oliet    
    - 15' reminder ISR 2022 (Tbilisi) by Besik Dundua and Temur Kutsia
    - 15' discussion
    - 75' Business Meeting (memberships, auxiliary topics)

Participation

The meetings of the working group are public, with the single exception of the business meeting.

Chair and Co-Chair/Secretary

Cynthia Kop and Carsten Fuhs