Preface

This volume contains the post-proceedings of two events: the 18^th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2023) and the 10^th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2023).

LSFA 2023

LSFA 2023 was held on July 1-2, 2023 in Rome, Italy, organized by the Sapienza Università di Roma and co-located with FSCD 2023, the 8th International Conference on Formal Structures for Computation and Deduction. The aim of the LSFA series of workshops is to bring together researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include proof theory, type theory and rewriting theory, specification and deduction languages, and formal semantics of languages and systems. For LSFA 2023, six regular papers were accepted for presentation out of ten submissions, with three reviewers per submission. After the meeting, revised versions of the papers were reviewed again, from which five regular papers were finally included in this volume. In addition, the workshop program included three talks by distinguished invited speakers Pablo Barenbaum (Universidad de Buenos Aires), Cynthia Kop (Radboud University Nijmegen), and Brigitte Pientka (McGill University). We express our sincere gratitude to them.

We want to thank the PC members and the additional reviewers for doing a great job providing high-quality reviews. Many thanks to the LSFA 2023 organizers, Daniele Nantes Sobrinho and David Cerna, the FSCD 2023 General Chair Daniele Gorla, and the FSCD Workshop Chair Ivano Salvo. All their valuable time spent was indispensable in guaranteeing the success of the workshop.

Temur Kutsia
Daniel Ventura
(LSFA 2023 PC co-chairs)

Program committee

External Reviewers

André Luiz Galdino, Jonathan Laurent

Organization

HCVS 2023

The workshop on Horn clauses for verification and synthesis (HCVS) series aims to bring together researchers working in the two communities of constraint/ logic programming (e.g., ICLP and CP), program verification (e.g., CAV, TACAS, and VMCAI), and automated deduction (e.g., CADE, IJCAR), on the topics of Horn clause based analysis, verification, and synthesis.

The 10^th edition took place on Sunday 23, April 2023 at the Institut Henri Poincaré in Paris, France, as part of ETAPS (European joint conferences on theory and practice of software). The workshop had received 7 submissions, 6 of which had been selected for presentation. Participants could opt for presentation-only or publication in proceedings. The program was supplemented by invited presentations.

We want to thank the PC members and additional reviewers for doing a great job providing high-quality reviews. The ETAPS local organization was splendid. We also thank Institut Henri Poincaré for providing the venue.

David Monniaux
Jose F. Morales
(HCVS 2023 PC co-chairs)

Program committee

Proof Terms for Higher-Order Rewriting and Their Equivalence

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. In this joint work with Eduardo Bonelli, we study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink’s, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (β-equivalence). This led Bruggink to reject “nested” composition, other than at the outermost level. We propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide.

Cutting a Proof into Bite-Sized Chunks (Incrementally Proving Termination in Higher-Order Term Rewriting)

In this talk, I will discuss a number of methods to prove termination of higher-order term rewriting systems, with a particular focus on large systems. In first-order term rewriting, the dependency pair framework can be used to split up a large termination problem into multiple (much) smaller components that can be solved individually. This is important because a large problem may take exponentially longer to solve in one go than solving each of its components.

Unfortunately, while there are higher-order versions of several of these methods, they often fail to simplify a problem enough. Here, we will explore some of these techniques and their limitations, and discuss what else can be done to incrementally build a termination proof for higher-order systems.

Mechanizing Session-Types: Enforcing Linearity without Linearity

Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent processes. Session types allow us to statically verify that processes communicate according to prescribed protocols. Hence, they rule out a wide class of communication-related bugs before executing a given process. They also statically guarantee safety properties such as session fidelity and deadlock freedom, analogous to preservation and progress in the simply typed lambda-calculus.

Although there have been many efforts to mechanize process calculi such as the pi-calculi in proof assistants, mechanizing these systems remains an art. Process calculi use channel or action names to specify process interactions, and they often feature rich binding structures and semantics such as channel mobility. Both of these features can be challenging to mechanize, for we must track names to avoid conflicts, ensure that alpha-equivalence and renaming are well-defined, etc. Moreover, session types employ a linear type system, where variables cannot be implicitly copied or dropped, and therefore, many mechanizations of these systems require modeling the context and carefully ensuring that its variables are handled linearly.

In this talk, I demonstrate a technique to localize linearity conditions as additional predicates embedded within type judgments, which allows us to use unrestricted typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higher-order abstract syntax to defer the intricate channel mobility and bindings that arise in a session typed system. In particular, I discuss the mechanization of a session typed system based on classical linear logic in the proof assistant Beluga, which uses the logical framework LF as its encoding language.

This is joint work with Chuta Sano and Ryan Kavanagh and is based on [Sano et al., 2023].

Data Abstraction, Arrays, Maps, and Completeness, aka "Cell Morphing"

(Invited talk abstract. This discusses joint work with Laure Gonnord and Julien Braine.)

Arrays and array-like data structures (such as hash-tables) are widely used in software. Furthermore, many semantic aspects of programming, such as byte-addressed memory, data structure fields, etc., can be modeled as arrays. Static analyzers that aim at proving properties of programs thus often need to deal with arrays. An array, in our context, is a map a from an index set I (not necessarily an integer range) to a value set V, with “get” a[i] and “set” a[i ← v] operations satisfying the relations:
a[i ← v][i] = v

a[i ← v][i′] = t[i′] when i′ ≠ i

Many interesting invariants about arrays are universally quantified over indices. For instance, “the array a contains 42 at all indices from 0 included to n excluded” is written ∀k, 0 ≤ k < n ⇒ a[k] = 42”; “the array a is sorted from indices from 0 included to n excluded” can be written ∀k₁k₂, 0 ≤ k₁ ≤ k₂ < n ⇒ a[k₁] ≤ a[k₂]. More generally, we consider invariants of the form ∀k₁, …_,k_mP(k₁, …, k_m, a[k₁], …, a[k_m], v₁, …, v_|V|) where a is an array and the v_i are other variables of the program, and P is an arbitrary predicate. We also consider the case of multiple arrays, so as to be able to express properties such as ∀k, 0 ≤ k < n ⇒ a[k] = b[k].

Numerous approaches have been proposed to automatically infer such invariants. We have proposed an approach (Braine, Gonnord, and Monniaux 2021, 2016; Braine 2022; Monniaux and Gonnord 2016), that converts an invariant inference problem (expressed as a solution to a system of Horn clauses), constrained by a safety property and restricted to such universally quantified invariants into an invariant inference problem on ordinary invariants (without universal quantification), through suitable quantifier instantiation. By further processing, through Ackermannization, these problems can even be converted, without loss of precision, to invariant inference problems over purely scalar variables (no more arrays).

While that second step does not incur loss of precision, the first step (quantifier instantiation), is in general sound (if the transformed invariant problem has a solution, then so has the original problem) but incomplete: it may be the case that it converts an invariant inference problem (a system of Horn clauses) that has a solution among universally quantified array invariants into a problem that has no solution. We however show that under certain syntactic restrictions (mostly, that the original Horn clause problem should be linear, which includes all problems obtained from the inductiveness conditions of control-flow graphs), that transformation is complete.

We thus show that under these conditions, our approach for solving invariant inference problems within universally quantified array properties is thus relatively complete to our ability to solve the resulting array-free ordinary invariant inference problem, in general over non-linear Horn clauses. This is the main limitation to our approach, since solvers for such kinds of problems tend to have unpredictable performance.