Cover Image

Tail Modulo Cons, OCaml, and Relational Separation Logic

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Allain, Clément, Bour, Frédéric, Clément, Basile, Pottier, François, Scherer, Gabriel
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

An Encoding of Interaction Nets in OCaml
by: Huber, Nikolaus, et al.
Published: (2025)

Mica: Automated Differential Testing for OCaml Modules
by: Ng, Ernest, et al.
Published: (2024)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
by: de Vilhena, Paulo Emílio, et al.
Published: (2021)

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
by: Chirica, Ion, et al.
Published: (2025)

How to benchmark: the Measure-Explain-Test-Improve loop
by: Scherer, Gabriel
Published: (2026)

Precise Reasoning About Container-Internal Pointers with Logical Pinning
by: Guan, Yawen, et al.
Published: (2025)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
by: Teuber, Samuel, et al.
Published: (2025)

Context-Aware Separation Logic
by: Meyer, Roland, et al.
Published: (2023)

Hyper Separation Logic (extended version)
by: Gospodinov, Trayan, et al.
Published: (2026)

Incremental Proof Development in Dafny with Module-Based Induction
by: Ho, Son, et al.
Published: (2024)

Automatic layout of railroad diagrams
by: Chiplunkar, Shardul, et al.
Published: (2025)

Beyond Cons: Purely Relational Data Structures
by: Sanna, Rafaello, et al.
Published: (2025)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
by: Ramananandro, Tahina, et al.
Published: (2025)

Verification Algorithms for Automated Separation Logic Verifiers
by: Eilers, Marco, et al.
Published: (2024)

Linear Matching of JavaScript Regular Expressions
by: Barrière, Aurèle, et al.
Published: (2023)

Verified Purely Functional Catenable Real-Time Deques
by: Viennot, Jules, et al.
Published: (2025)

Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
by: Barrière, Aurèle, et al.
Published: (2025)

On the computational complexity of JavaScript regex matching
by: Deng, Victor, et al.
Published: (2026)

Formal Foundations for Translational Separation Logic Verifiers (extended version)
by: Dardinier, Thibault, et al.
Published: (2024)

Recursive Mutexes in Separation Logic
by: Du, Ke, et al.
Published: (2026)

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
by: Wu, Shushu, et al.
Published: (2025)

Logical Relations for Session-Typed Concurrency
by: Balzer, Stephanie, et al.
Published: (2023)

Modeling Reachability Types with Logical Relations
by: Bao, Yuyan, et al.
Published: (2023)

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
by: Ling, Hongyi, et al.
Published: (2026)

A Coq Mechanization of JavaScript Regular Expression Semantics
by: De Santo, Noé, et al.
Published: (2024)

Close is Good Enough: Component-Based Synthesis Modulo Logical Similarity
by: Mishra, Ashish, et al.
Published: (2025)

Towards Concurrent Quantitative Separation Logic
by: Fesefeldt, Ira, et al.
Published: (2022)

Tracers for debugging and program exploration
by: Chiplunkar, Shardul, et al.
Published: (2026)

Omnidirectional type inference for ML: principality any way
by: O'Brien, Alistair, et al.
Published: (2025)

Agentic Separation Logic Specification Synthesis
by: Suresh, Tarun, et al.
Published: (2026)

A Nominal Approach to Probabilistic Separation Logic
by: Li, John M., et al.
Published: (2024)

Unboxed data constructors -- or, how cpp decides a halting problem
by: Chataing, Nicolas, et al.
Published: (2023)

On Computational Indistinguishability and Logical Relations
by: Lago, Ugo Dal, et al.
Published: (2024)

Stellis: A Strategy Language for Purifying Separation Logic Entailments
by: Wang, Zhiyi, et al.
Published: (2025)

Source-to-Source Transformations for GPU Code Generation
by: de Castelnau, Julien, et al.
Published: (2026)

Teaching Synchronous Dataflow Modelling with Learn-Heptagon
by: Garoche, Pierre-Loïc, et al.
Published: (2026)

A Language-Agnostic Logical Relation for Message-Passing Protocols
by: Zhang, Tesla, et al.
Published: (2025)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
by: Le, Quang Loc
Published: (2025)

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)