| Robbert Krebbers, Radboud University Nijmegen, The Netherlands |
| Mechanized Type Soundness for Substructural Types using Iris |
|
Substructural type systems are a good fit to enforce strong safety properties of higher-order, imperative and concurrent programs. Key examples are the Rust type system (which enforces the absence of undefined behavior and data races) and session types (which enforce correct usage of message-passing channels). Formally proving that these type systems "do their job" (i.e., they enjoy the "type soundness" property) challenging. This challenge is exacerbated when considering combinations of language features ("feature interaction") and linking against "unsafe" libraries (which have to be verified manually), thus providing the desire for a scalable approach with support for machine-checked proofs. In this talk I will give an introduction to the "logical approach" to type soundness, which is well-suited to prove soundness of substructural type systems. I will explain the theory of the logical approach in the context of a very simple language, which I then gradually scale up to a session-typed language. I will also demonstrate that the logical approach is well-suited for the mechanization of challenging type systems in the Rocq prover using the Iris framework for concurrent separation logic. |
| José Meseguer, University of Illinois Urbana-Champaign, IL, US |
| Symbolic Computation and Verification Methods in Maude |
|
Maude and its formal tools support ten different symbolic computation features. This paper focuses on one of them, narrowing of constrained patterns, as well as its combination with inductive theorem proving in a novel style of deductive model checking, to illustrate how Maude's symbolic features can be used to model check modal logic properties of infinite-state systems specified as rewrite theories in Maude. |
TUESDAY, SEPTEMBER 9 |
|
|---|---|
| 09:30-10:30 |
José Meseguer (invited speaker)
Symbolic Computation and Verification Methods in Maude |
| 10:30-11:00 | COFFEE BREAK |
|
Session 1 - Rewriting
Chairs: TBA |
|
| 11:00-11:30 |
Maribel Fernández, Daniele Nantes Sobrinho and Daniella Santaguida
A Completion Procedure for Equational Rewriting Systems with Binders |
| 11:30-12:00 |
Etienne Payet
Recurrent Pairs Revisited |
| 12:00-12:30 |
Kanta Takahata, Jonas Schöpf, Naoki Nishida and Takahito Aoto
Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms |
| 13:00-14:30 | LUNCH |
|
Session 2 - Program Synthesis
Chairs: TBA |
|
| 14:30-15:00 |
Romain Pascual, Pascale Le Gall, Hakim Belhaouari and Agnès Arnould
Program synthesis for geometric modeling |
| 15:00-15:30 |
Evgeny Skvortsov, Ojaswa Garg, Shayan Mirjafari, Yilin Xia, Shawn Bowers and Bertram Ludäscher
Logica and LogicLM Program Synthesis Evaluation |
| 15:30-16:00 |
Paul Tarau
Focusing Recursive LLM Descents with Plans Expressed as Logic Programs |
| 16:30-17:00 | COFFEE BREAK |
WEDNESDAY, SEPTEMBER 10 |
|
|---|---|
| 09:30-10:30 |
Robbert Krebbers (invited speaker joint with PPDP)
TBA |
| 10:30-11:00 | COFFEE BREAK |
|
Session 3 - Verification and Analysis
Chairs: TBA |
|
| 11:00-11:30 |
Elvira Albert, Emanuele De Angelis, Fabio Fioravanti, Alejandro Hernández-Cerezo and Giulia Matricardi
Verifying Smart Contracts in Yul via Transformation to CHC by Interpreter Specialization |
| 11:30-12:00 |
Michael Hanus
Managing Analysis and Verification Information about Curry Packages (System Description) |
| 12:00-12:30 |
Thierry Marianne, Fred Mesnard and Etienne Payet
Automated Certification of Logic Programs Groundness Analysis |
| 13:00-14:30 | LUNCH |
|
Session 4 - Logic Programming and Extensions
Chairs: TBA |
|
| 14:30-15:00 |
Besik Dundua and Temur Kutsia
Higher-Order Pattern Unification Modulo Similarity Relations |
| 15:00-15:30 |
Angelos Charalambidis, Georgios Nikolaou and Antonis Troumpoukis
Implementing a Many-Valued Semantics for Logic Programs with Ordered Disjunction Using ASP |
| 15:30-16:00 |
Paula Corral, Jose F. Morales, Pedro Lopez-Garcia and Manuel V. Hermenegildo
Extending the FSyntax/Hiord Approach with Imperative Notation |
| 16:30-17:00 | COFFEE BREAK |
| 18:30 | EXCURSION AND SOCIAL DINNER |
The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in logic-based program development in any language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress.
LOPSTR 2025 will be held in-person at University of Calabria in Rende, Italy and will be co-located with PPDP 2025 and ICLP 2025. At least one of the authors of an accepted paper is required to attend the conference and present the paper. Information about venue and travel will be made available later.
Topics of interest cover all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large, including, but not limited to:
Survey papers that present some aspects of the above topics from a new perspective and papers that describe experience with industrial applications and case studies are also welcome.
LOPSTR is a renowned symposium that has been held for more than 30 years. The first meeting was held in Manchester, UK in 1991. Information about previous symposia can be found here. You can have a look at the contents of past LOPSTR symposia at DBLP and past LNCS proceedings at the Springer repository.
The important conference dates are as follows. All deadlines are AoE.
The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions to logic-based program development in any programming language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress.
LOPSTR 2025 will be held at the University of Calabria, Rende, Italy. It will be co-located with ICLP 2025 and PPDP 2025. At least one of the authors of an accepted paper is expected to attend the conference and present the paper. Information about venue and travel will be available on the ICLP 2025 website.
Topics of interest include all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large, including, but not limited to:
Submissions can be made in two categories:
References will NOT count towards the page limit. Additional pages may be used for appendices not intended for publication. Reviewers are not required to read the appendices, and thus papers should be intelligible without them. All submissions must be written in English.
Submissions must not substantially overlap with papers/tools that have been published or that are simultaneously submitted to a journal, conference, or workshop with refereed proceedings.
Submissions of Regular Papers must describe original work. Work that already appeared in unpublished or informally published workshop proceedings may be submitted (please contact the PC Chairs in case of questions).
Submissions of Short Papers may include presentations of exciting if not fully polished research or tool demonstrations that are of academic and industrial interest. Tool demonstrations should describe the relevant system, usability, and implementation aspects of a tool.
All accepted papers will be included in the conference proceedings and published by Springer as a Lecture Notes in Computer Science (LNCS) volume.
After the symposium, a selection of a few best papers will be invited for submission to rapid publication in the Journal of Theory and Practice of Logic Programming (TPLP). Authors of selected papers will be invited to revise and/or extend their submissions to be considered for publication. The papers submitted to TPLP will be subject to the journal's standard reviewing process.
Authors should submit an electronic copy of the paper (written in English) in PDF, formatted in the Lecture Notes in Computer Science style. Each submission must include on its first page the paper title; authors and their affiliations; contact author's email; abstract; and three to four keywords which will be used to assist the PC in selecting appropriate reviewers for the paper.
Page numbers (and, if possible, line numbers) should appear on the manuscript to help the reviewers in writing their report. So, for LaTeX, we recommend that authors use:
\pagestyle{plain}
\usepackage{lineno}
\linenumbers
Papers should be submitted via EasyChair: https://easychair.org/conferences/?conf=lopstr2025
| Program Chairs | |
| Laura Titolo | Code Metal, Inc. |
| Santiago Escobar | Universitat Politècnica de València, Spain |
| Program Committee Members | |
| Elvira Albert | Complutense University of Madrid, Spain |
| Roberto Amadini | University of Bologna, Italy |
| João Barbosa | University of Porto, Portugal |
| Juliana Bowles | University of St. Andrews, UK |
| Wlodek Drabent | IPI PAN Warszawa, Poland |
| Catherine Dubois | ENSIIE-Samovar, France |
| Fabio Fioravanti | University of Chieti-Pescara, Italy |
| Mário Florido | University of Porto, Portugal |
| Gopal Gupta | University of Texas at Dallas, US |
| Michael Hanus | CAU Kiel, Germany |
| Bishoksan Kafle | University of Melbourne, Australia |
| Temur Kutsia | RISC, Johannes Kepler University Linz, Austria |
| Salvador Lucas | Universitat Politècnica de València, Spain |
| Fred Mesnard | Université de La Réunion, France |
| Julia Sapiña | Universitat Politècnica de València, Spain |
| Harald Søndergaard | University of Melbourne, Australia |
| Theresa Swift | Johns Hopkins Applied Physics Lab, US |
| Wim Vanhoof | Université de Namur, Belgium |
| Alicia Villanueva | Universitat Politècnica de València, Spain |