FLOC 2022: FEDERATED LOGIC CONFERENCE 2022
IFIP-WG1.6 ON SUNDAY, JULY 31ST

View: session overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 1E
Location: Ullmann 306
09:00
Inversion and Determinization in Term Rewriting

ABSTRACT. As a transformational approach, inversion is formulated in several settings, and the basic ideas are naive and similar. To generate a better form, e.g., non-overlapping systems if possible, determinization is used as a post-process of inversion for injective functions, and is the most challenging part in developing an inversion framework. In this talk, I introduce a framework of inversion and determinization in term rewriting. First, I explain a direct inversion of deterministic CTRSs, and a direct MSV-based determinization. Next, I explain the framework proposed by Gluck and Kawabe, which uses context-free grammars as intermediate representations of CTRSs. Finally, I explain a framework based on context-free expressions.

10:00
RLooP (the Rewriting List of open Problems)
10:30-11:00Coffee Break
11:00-12:30 Session 10G
Location: Ullmann 306
11:00
Quantitative Weak Linearisation

ABSTRACT. Weak linearisation was defined years ago through a static characterisation of the intuitive notion of virtual redex, based on (legal) paths computed from the (syntactical) term tree. Weak-linear terms impose a linearity condition only on functions that are applied (consumed by reduction) and functions that are not applied (therefore persist in the term along any reduction) can be non-linear. This class of terms was shown to be strongly normalising with deciding typability in polynomial time. We revisit this notion through non-idempotent intersection types (also called quantitative types). By using an effective characterisation of minimal typings, based on the notion of tightness, we are able to distinguish between “consumed” and “persistent” term constructors, which allows us to define an expansion relation, between general lambda-terms and weak-linear lambda-terms, whilst preserving normal forms by reduction.

12:00
The International School on Rewriting

ABSTRACT. This slot contains an advertisement for ISR in Tbilisi, a proposal and vote for ISR 2024, and perhaps a general discussion on the future of ISR.

12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

15:30-16:00Coffee Break
16:00-17:30 Session 19F

Business Meeting (IFIP-WG 1.6)

Location: Ullmann 306