The date for the annual meeting of the IFIP WG 1.6 is Monday, July 1, 2024. The meeting is co-located with IJCAR 2024, and will take place on the first workshop day.
Abstract: Probabilistic models play a crucial role to reason under uncertainty. This talk relies on rewriting theory and semantical techniques to relate two such models: on the one hand, *probabilistic programming languages*, where statistical models are specified as programs, on the other hand *Bayesian networks*, a prominent tool for probabilistic reasoning, allowing for a compact (factorized) representation of large probability distributions, and for efficient inference algorithms.
The goal is integrating the efficiency of Bayesian networks---which are graphical first-order models---with the expressiveness of higher-order functional programming. Ideally, the design of the Bayesian model should be carried at high-level, in the functional language, which provides recursion and expressive constructs. Higher-order terms then compile (i.e. rewrite) into Bayesian networks, which serve as the low-level language. The groundwork for the compilation scheme are semantical tools, in particular rewriting theory and type systems.
(This talk reports on work in collaboration with Ehrhard, Pagani, Pautasso, Vanoni.)
Abstract: Center-stage of my talk will be a structural property of process graphs that are interpretations of regular expressions: the loop existence and elimination condition (LEE). It turned out to be instrumental for tackling axiomatization and recognition problems for Milner's process semantics of regular expressions. Next to indicating its role in my work on these problems, I want to explain how concepts and ideas from rewriting are crucial for the definition of LEE and the study of its properties.
LEE is defined by a terminating loop-subgraph-elimination rewrite system. This system can be completed into a confluent system, which entails that LEE is efficiently decidable. Process interpretations of regular expressions satisfy LEE if they are `under-star-1-free', and in general if they satisfy a refinement property 1-LEE, which requires of a process graph to be refinable into a graph with LEE by means of increasing sharing through added 1-transitions (empty steps). `LEE-witnesses' are labelings of process graphs that satisfy LEE. They guarantee expressibility by a regular expression: every process graph G with a LEE-witness facilitates the efficient extraction of a regular expression whose process interpretation is bisimilar to G. Two further lemmas are of critical importance for obtaining completeness results. First, LEE is preserved under bisimulation collapse; this can be established by a stepwise collapse procedure. However, second, 1-LEE is not preserved under bisimulation collapse.
Finally I report on a recent technical refinement of the extraction procedure that permits to understand LEE/1-LEE as characteristic properties for the restricted/unrestricted images of a (slightly more) compact version of the process interpretation. LEE (and resp. 1-LEE) characterizes those process graphs that are isomorphic to compact process interpretations of under-star-1-free regular expressions (resp. that refine compact process interpretations of arbitrary regular expressions).
Abstract: Maude is a language and a system based on rewriting logic. It is a mathematical modeling language thanks to its logical basis and its initial model semantics. Maude can be used in three, mutually reinforcing ways: as a declarative programming language, as an executable formal specification language, and as a formal verification system. Logical reasoning capabilities have been recently added to Maude. This talk gives an overview of the different unification and narrowing techniques available in Maude 3.4, focusing on some of the programming, modeling, and verification aspects of Maude.
Abstract: In this talk, I will present recent research on the expressivity of concurrent languages, utilizing a session-typed pi-calculus that incorporates non-determinism and failure behaviour. Building on an extension of Milner's encoding from the pi-calculus to the lambda-calculus, we have discovered a novel relationship between session types and intersection types. This research introduces a translation from the session-typed pi-calculus to a resource-aware lambda-calculus with intersection types. Our translation preserves typability and operational correspondence, enabling the transfer of dynamic properties between these two languages.
Abstract: Saturation theorem provers process a set of formulas by repeatedly performing two operations: first, by applying inference rules to formulas in the set, whose conclusions are then added to the set; second, by deleting formulas that are redundant, which means that they can be shown to be unnecessary to derive a contradiction. The relationship between redundancy, saturation, and static and dynamic refutational completeness was established by Bachmair and Ganzinger in the 1990s. The abstract framework for saturation theorem proving that we presented in 2020 extends the work by Bachmair and Ganzinger. In my talk, I will discuss the framework, its history, applications, and recent developments and extensions.
09:00 - 10:30: Session 1
- 45' Claudia Faggian
- 45' Clemens Grabmayer
10:30 - 11:00: Coffee Break
11:00 - 12:30: Session 2
- 45' Santiago Escobar
- 45' Daniele Nantes
12:30 - 14:00: Lunch Break
14:00 - 16:00: Session 4
- 45' Uwe Waldmann
- 30' The International School on Rewriting
- 45' Jean-Pierre Jouannaud: Rooted Graph Rewriting
16:00 - 16:30: Coffee Break
16:30 - 17:30: Business Meeting
(only for members of the working group)
The meetings of the working group are public, with the single exception of the business meeting. The presentations are all in-person, but will be livestreamed.