2026-07-22T18:35:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24625 2025-09-22T06:50:21Z ddc:004 open_access

Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic Krebbers, Robbert van der Maas, Luko Tassi, Enrico Separation Logic Program Verification Data Structures Iris Rocq prover Inductive predicates play a key role in program verification using separation logic. There are many methods for defining such predicates in separation logic, which all have different conditions and thus support different classes of predicates. The most common methods are: (1) through a structurally-recursive definition (commonly used to define representation predicates for the verification of data structures), and (2) through step-indexing (commonly used to give a semantics of Hoare triples for partial program correctness). A lesser-known method is to define such inductive predicates internally in higher-order separation logic through a least fixpoint of a monotone function. The contributions of this paper are fourfold. First, we present the folklore result (from the Iris library) that one can define least (and greatest) fixpoints internally in separation logic by extending the standard second-order impredicative encoding with some modalities. Second, we show that these fixpoints are useful to define representation predicates where the mathematical and in-memory data structures do not correspond. Third, we show that these fixpoints can be used to define Hoare triples and weakest preconditions for total program correctness in Iris. Fourth, we present a prototype command (akin to Rocq’s Inductive), written in Rocq-Elpi, to generate the least fixpoint and its reasoning principles (constructors and induction principles) from a high-level specification. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robbert Krebbers and Luko van der Maas and Enrico Tassi 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.27 urn:nbn:de:0030-drops-246258 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.27 eng https://creativecommons.org/licenses/by/4.0/legalcode