Document Open Access Logo

Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic

Authors Robbert Krebbers , Luko van der Maas , Enrico Tassi

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.27.pdf
  • Filesize: 0.98 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Programming logic
Keywords
  • Separation Logic
  • Program Verification
  • Data Structures
  • Iris
  • Rocq prover

Metrics

Abstract

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.

Cite As Get BibTex

Robbert Krebbers, Luko van der Maas, and Enrico Tassi. Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 27:1-27:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.27

Author Details

Robbert Krebbers
  • Radboud University, Nijmegen, The Netherlands
Luko van der Maas
  • Radboud University, Nijmegen, The Netherlands
Enrico Tassi
  • Université Côte d'Azur, Inria, Nice, France

Funding

This work is supported in part by ERC grant COCONUT (grant no. 101171349), funded by the European Union, and NWO grant FuRoRe (OCENW.M.22.282). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them.

Acknowledgements

We thank Ralf Jung and Jacques-Henri Jourdan for early discussions about fixpoints in Iris, Aleš Bizjak for suggesting to define weakest preconditions using a least fixpoint, and the anonymous reviewers for their feedback.

Supplementary Materials

References

  1. Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal. Error credits: Resourceful reasoning about error bounds for higher-order probabilistic programs. PACMPL, 8(ICFP):284-316, 2024. URL: https://doi.org/10.1145/3674635.
  2. Amal Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004. Google Scholar
  3. Andrew W. Appel. Tactics for separation logic, 2006. Unpublished manuscript. URL: http://www.cs.princeton.edu/~appel/papers/septacs.pdf.
  4. Andrew W. Appel and David A. McAllester. An indexed model of recursive types for foundational proof-carrying code. TOPLAS, 23(5):657-683, 2001. URL: https://doi.org/10.1145/504709.504712.
  5. Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, and Jérôme Vouillon. A very modal model of a modern, major, general type system. In Martin Hofmann and Matthias Felleisen, editors, POPL, pages 109-122, 2007. URL: https://doi.org/10.1145/1190216.1190235.
  6. Robert Atkey. Amortised resource analysis with separation logic. LMCS, 7(2), 2011. URL: https://doi.org/10.2168/LMCS-7(2:17)2011.
  7. David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In LPAR, volume 4790 of LNCS, pages 92-106, 2007. URL: https://doi.org/10.1007/978-3-540-75560-9_9.
  8. Jesper Bengtson, Jonas Braband Jensen, and Lars Birkedal. Charge! - A framework for higher-order separation logic in Coq. In ITP, volume 7406 of LNCS, pages 315-331, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_21.
  9. Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL - lessons learned in formal-logic engineering. In TPHOLs, volume 1690 of LNCS, pages 19-36, 1999. URL: https://doi.org/10.1007/3-540-48256-3_3.
  10. Bodil Biering, Lars Birkedal, and Noah Torp-Smith. BI-hyperdoctrines, higher-order separation logic, and abstraction. TOPLAS, 29(5):24, 2007. URL: https://doi.org/10.1145/1275497.1275499.
  11. Stephen Brookes. A semantics for concurrent separation logic. TCS, 375(1-3):227-270, 2007. URL: https://doi.org/10.1016/J.TCS.2006.12.034.
  12. Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. VST-Floyd: A separation logic tool to verify correctness of C programs. JAR, 61(1-4):367-422, 2018. URL: https://doi.org/10.1007/S10817-018-9457-5.
  13. Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying concurrent, crash-safe systems with perennial. In SOSP, pages 243-258, 2019. URL: https://doi.org/10.1145/3341301.3359632.
  14. Arthur Charguéraud. Program verification through characteristic formulae. In ICFP, pages 321-332, 2010. URL: https://doi.org/10.1145/1863543.1863590.
  15. Arthur Charguéraud. Higher-order representation predicates in separation logic. In CPP, pages 3-14, 2016. URL: https://doi.org/10.1145/2854065.2854068.
  16. Arthur Charguéraud. Separation logic for sequential programs (functional pearl). PACMPL, 4(ICFP):116:1-116:34, 2020. URL: https://doi.org/10.1145/3408998.
  17. Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter. Omnisemantics: Smooth handling of nondeterminism. TOPLAS, 45(1):5:1-5:43, 2023. URL: https://doi.org/10.1145/3579834.
  18. Arthur Charguéraud and François Pottier. Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. JAR, 62(3):331-365, 2019. URL: https://doi.org/10.1007/S10817-017-9431-7.
  19. Adam Chlipala. The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In ICFP, pages 391-402, 2013. URL: https://doi.org/10.1145/2500365.2500592.
  20. Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In FSCD, volume 167 of LIPIcs, pages 34:1-34:21, 2020. URL: https://doi.org/10.4230/LIPICS.FSCD.2020.34.
  21. Thierry Coquand and Gérard P. Huet. The Calculus of Constructions. I&C, 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  22. Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In COLOG-88, pages 50-66, 1990. URL: https://doi.org/10.1007/3-540-52335-9_47.
  23. Paulo Emílio de Vilhena and François Pottier. A separation logic for effect handlers. PACMPL, 5(POPL):1-28, 2021. URL: https://doi.org/10.1145/3434314.
  24. Emanuele D'Osualdo, Julian Sutherland, Azadeh Farzan, and Philippa Gardner. TaDA Live: Compositional reasoning for termination of fine-grained concurrent programs. TOPLAS, 43(4):16:1-16:134, 2021. URL: https://doi.org/10.1145/3477082.
  25. Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. ELPI: fast, embeddable, λprolog interpreter. In LPAR, volume 9450 of LNCS, pages 460-468, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_32.
  26. David Fissore and Enrico Tassi. A new type-class solver for Coq in Elpi. In Coq Workshop, 2023. URL: https://inria.hal.science/hal-04467855.
  27. Dan Frumin, Robbert Krebbers, and Lars Birkedal. Compositional non-interference for fine-grained concurrent programs. In S&P, pages 1416-1433, 2021. URL: https://doi.org/10.1109/SP40001.2021.00003.
  28. Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. Simuliris: A separation logic framework for verifying concurrent program optimizations. PACMPL, 6(POPL):1-31, 2022. URL: https://doi.org/10.1145/3498689.
  29. Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal. Mechanized logical relations for termination-insensitive noninterference. PACMPL, 5(POPL):1-29, 2021. URL: https://doi.org/10.1145/3434291.
  30. Benjamin Grégoire, Jean-Christophe Léchenet, and Enrico Tassi. Practical and sound equality tests, automatically: Deriving eqType instances for Jasmin’s data types with Coq-Elpi. In CPP, pages 167-181, 2023. URL: https://doi.org/10.1145/3573105.3575683.
  31. Elsa L. Gunter. A broader class of trees for recursive type definitions for HOL. In HUG, volume 780 of LNCS, pages 141-154, 1993. URL: https://doi.org/10.1007/3-540-57826-9_131.
  32. Timothy L. Harris. A pragmatic implementation of non-blocking linked-lists. In DISC, volume 2180 of LNCS, pages 300-314, 2001. URL: https://doi.org/10.1007/3-540-45414-4_21.
  33. John Harrison. Inductive definitions: Automation and application. In TPHOL, volume 971 of LNCS, pages 200-213, 1995. URL: https://doi.org/10.1007/3-540-60275-5_66.
  34. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Connectivity graphs: a method for proving deadlock freedom based on separation logic. PACMPL, 6(POPL):1-33, 2022. URL: https://doi.org/10.1145/3498662.
  35. Ralf Jung. Iris Merge Request 60: "Implement greatest fixed point inside the logic", 2017. URL: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/60.
  36. Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. Higher-order ghost state. In ICFP, pages 256-269, 2016. URL: https://doi.org/10.1145/2951913.2951943.
  37. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP, 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  38. Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. The future is ours: Prophecy variables in separation logic. PACMPL, 4(POPL):45:1-45:32, 2020. URL: https://doi.org/10.1145/3371113.
  39. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL, pages 637-650, 2015. URL: https://doi.org/10.1145/2676726.2676980.
  40. Bronisław Knaster. Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématique, 6:133-134, 1928. Google Scholar
  41. Robbert Krebbers. Iris commit 1e8054db: "Port fixpoints to BIs", 2017. URL: https://gitlab.mpi-sws.org/iris/iris/-/commit/1e8054db.
  42. Robbert Krebbers. Iris Merge Request: "Weakest preconditions for total program correctness", 2017. URL: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/65.
  43. Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. MoSeL: A general, extensible modal framework for interactive proofs in separation logic. PACMPL, 2(ICFP):77:1-77:30, 2018. URL: https://doi.org/10.1145/3236772.
  44. Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. The essence of higher-order concurrent separation logic. In ESOP, volume 10201 of LNCS, pages 696-723, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_26.
  45. Robbert Krebbers, Amin Timany, and Lars Birkedal. Interactive proofs in higher-order concurrent separation logic. In POPL, pages 205-217, 2017. URL: https://doi.org/10.1145/3009837.3009855.
  46. Robbert Krebbers, Luko van der Maas, and Enrico Tassi. Rocq development of "Inductive predicates via least fixpoints in higher-order separation logic", 2025. URL: https://doi.org/10.5281/zenodo.15727403.
  47. Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308-320, 1964. URL: https://doi.org/10.1093/COMJNL/6.4.308.
  48. Hongjin Liang and Xinyu Feng. Progress of concurrent objects with partial methods. PACMPL, 2(POPL):20:1-20:31, 2018. URL: https://doi.org/10.1145/3158108.
  49. Thomas F. Melham. A package for inductive relation definitions in HOL. In TPHOL, pages 350-357, 1991. Google Scholar
  50. Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in Iris. In ESOP, volume 11423 of LNCS, pages 3-29, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_1.
  51. Hiroshi Nakano. A modality for recursion. In LICS, pages 255-266, 2000. URL: https://doi.org/10.1109/LICS.2000.855774.
  52. Peter W. O'Hearn. Resources, concurrency, and local reasoning. TCS, 375(1-3):271-307, 2007. URL: https://doi.org/10.1016/J.TCS.2006.12.035.
  53. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bull. Symb. Log., 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  54. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL, volume 2142 of LNCS, pages 1-19, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  55. Christine Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In TLCA, volume 664 of LNCS, pages 328-345, 1993. URL: https://doi.org/10.1007/BFB0037116.
  56. Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In CADE, volume 814 of LNCS, pages 148-161, 1994. URL: https://doi.org/10.1007/3-540-58156-1_11.
  57. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In PLDI, pages 199-208, 1988. URL: https://doi.org/10.1145/53990.54010.
  58. Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In MFPS, volume 442 of LNCS, pages 209-228, 1989. URL: https://doi.org/10.1007/BFB0040259.
  59. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55-74, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  60. Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. Intrinsically-typed definitional interpreters for linear, session-typed languages. In CPP, pages 284-298, 2020. URL: https://doi.org/10.1145/3372885.3373818.
  61. Kazuhiko Sakaguchi. Reflexive tactics for algebra, revisited. In ITP, volume 237 of LIPIcs, pages 29:1-29:22, 2022. URL: https://doi.org/10.4230/LIPICS.ITP.2022.29.
  62. Thomas Somers and Robbert Krebbers. Verified lock-free session channels with linking. PACMPL, 8(OOPSLA2):588-617, 2024. URL: https://doi.org/10.1145/3689732.
  63. Matthieu Sozeau. A new look at generalized rewriting in type theory. JFR, 2(1):41-62, 2009. URL: https://doi.org/10.6092/ISSN.1972-5787/1574.
  64. Matthieu Sozeau and Nicolas Oury. First-class type classes. In TPHOLs, volume 5170 of LNCS, pages 278-293, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_23.
  65. Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. In PLDI, pages 80-95, 2021. URL: https://doi.org/10.1145/3453483.3454031.
  66. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 2:285-309, 1955. URL: https://doi.org/10.2140/pjm.1955.5.285.
  67. Joseph Tassarotti and Robert Harper. A separation logic for concurrent randomized programs. PACMPL, 3(POPL):64:1-64:30, 2019. URL: https://doi.org/10.1145/3290377.
  68. Joseph Tassarotti, Ralf Jung, and Robert Harper. A higher-order logic for concurrent termination-preserving refinement. In ESOP, volume 10201 of LNCS, pages 909-936, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_34.
  69. Enrico Tassi. Elpi: An extension language for Coq (metaprogramming Coq in the Elpi λProlog dialect). In CoqPL, 2018. URL: https://inria.hal.science/hal-01637063.
  70. Enrico Tassi. Deriving proved equality tests in Coq-Elpi: Stronger induction principles for containers in Coq. In ITP, volume 141 of LIPIcs, pages 29:1-29:18, 2019. URL: https://doi.org/10.4230/LIPICS.ITP.2019.29.
  71. Enrico Tassi. Elpi: Rule-based meta-language for Rocq. In CoqPL, 2025. URL: https://inria.hal.science/hal-04990628.
  72. The Rocq Prover development team. Rocq 9.0.0 reference manual, section inductive types and recursive functions, 2026. URL: https://rocq-prover.org/doc/V9.0.0/refman/language/core/inductive.html.
  73. The std++ developers and contributors. Rocq-std++: An extended "Standard Library" for Rocq, 2024. URL: https://gitlab.mpi-sws.org/iris/stdpp/.
  74. Amin Timany and Lars Birkedal. Mechanized relational verification of concurrent programs with continuations. PACMPL, 3(ICFP):105:1-105:28, 2019. URL: https://doi.org/10.1145/3341709.
  75. Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, and Lars Birkedal. Trillium: Higher-order concurrent and distributed separation logic for intensional refinement. PACMPL, 8(POPL):241-272, 2024. URL: https://doi.org/10.1145/3632851.
  76. Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette. Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In LICS, pages 596-605, 2012. URL: https://doi.org/10.1109/LICS.2012.75.
  77. Luko van der Maas. Extending the Iris Proof Mode with inductive predicates using Elpi. Master’s thesis, Radboud University Nijmegen, 2024. URL: https://doi.org/10.5281/zenodo.15727560.
  78. Orpheas van Rooij and Robbert Krebbers. Affect: An affine type and effect system. PACMPL, 9(POPL):126-154, 2025. URL: https://doi.org/10.1145/3704841.
  79. Max Vistrup, Michael Sammler, and Ralf Jung. Program logics à la carte. PACMPL, 9(POPL):300-331, 2025. URL: https://doi.org/10.1145/3704847.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact