Image de couverture de livre

Tail Modulo Cons, OCaml, and Relational Separation Logic

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Allain, Clément, Bour, Frédéric, Clément, Basile, Pottier, François, Scherer, Gabriel
Format:	Preprint
Publié:	2024
Sujets:	Programming Languages
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

An Encoding of Interaction Nets in OCaml
par: Huber, Nikolaus, et autres
Publié: (2025)

Mica: Automated Differential Testing for OCaml Modules
par: Ng, Ernest, et autres
Publié: (2024)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
par: de Vilhena, Paulo Emílio, et autres
Publié: (2021)

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
par: Chirica, Ion, et autres
Publié: (2025)

How to benchmark: the Measure-Explain-Test-Improve loop
par: Scherer, Gabriel
Publié: (2026)

Precise Reasoning About Container-Internal Pointers with Logical Pinning
par: Guan, Yawen, et autres
Publié: (2025)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
par: Teuber, Samuel, et autres
Publié: (2025)

Context-Aware Separation Logic
par: Meyer, Roland, et autres
Publié: (2023)

Hyper Separation Logic (extended version)
par: Gospodinov, Trayan, et autres
Publié: (2026)

Incremental Proof Development in Dafny with Module-Based Induction
par: Ho, Son, et autres
Publié: (2024)

Automatic layout of railroad diagrams
par: Chiplunkar, Shardul, et autres
Publié: (2025)

Beyond Cons: Purely Relational Data Structures
par: Sanna, Rafaello, et autres
Publié: (2025)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
par: Ramananandro, Tahina, et autres
Publié: (2025)

Verification Algorithms for Automated Separation Logic Verifiers
par: Eilers, Marco, et autres
Publié: (2024)

Linear Matching of JavaScript Regular Expressions
par: Barrière, Aurèle, et autres
Publié: (2023)

Verified Purely Functional Catenable Real-Time Deques
par: Viennot, Jules, et autres
Publié: (2025)

Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
par: Barrière, Aurèle, et autres
Publié: (2025)

On the computational complexity of JavaScript regex matching
par: Deng, Victor, et autres
Publié: (2026)

Formal Foundations for Translational Separation Logic Verifiers (extended version)
par: Dardinier, Thibault, et autres
Publié: (2024)

Recursive Mutexes in Separation Logic
par: Du, Ke, et autres
Publié: (2026)

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
par: Wu, Shushu, et autres
Publié: (2025)

Logical Relations for Session-Typed Concurrency
par: Balzer, Stephanie, et autres
Publié: (2023)

Modeling Reachability Types with Logical Relations
par: Bao, Yuyan, et autres
Publié: (2023)

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
par: Ling, Hongyi, et autres
Publié: (2026)

A Coq Mechanization of JavaScript Regular Expression Semantics
par: De Santo, Noé, et autres
Publié: (2024)

Close is Good Enough: Component-Based Synthesis Modulo Logical Similarity
par: Mishra, Ashish, et autres
Publié: (2025)

Towards Concurrent Quantitative Separation Logic
par: Fesefeldt, Ira, et autres
Publié: (2022)

Tracers for debugging and program exploration
par: Chiplunkar, Shardul, et autres
Publié: (2026)

Omnidirectional type inference for ML: principality any way
par: O'Brien, Alistair, et autres
Publié: (2025)

Agentic Separation Logic Specification Synthesis
par: Suresh, Tarun, et autres
Publié: (2026)

A Nominal Approach to Probabilistic Separation Logic
par: Li, John M., et autres
Publié: (2024)

Unboxed data constructors -- or, how cpp decides a halting problem
par: Chataing, Nicolas, et autres
Publié: (2023)

On Computational Indistinguishability and Logical Relations
par: Lago, Ugo Dal, et autres
Publié: (2024)

Stellis: A Strategy Language for Purifying Separation Logic Entailments
par: Wang, Zhiyi, et autres
Publié: (2025)

Source-to-Source Transformations for GPU Code Generation
par: de Castelnau, Julien, et autres
Publié: (2026)

Teaching Synchronous Dataflow Modelling with Learn-Heptagon
par: Garoche, Pierre-Loïc, et autres
Publié: (2026)

A Language-Agnostic Logical Relation for Message-Passing Protocols
par: Zhang, Tesla, et autres
Publié: (2025)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
par: Le, Quang Loc
Publié: (2025)

Reasoning about Weak Isolation Levels in Separation Logic
par: Mathiasen, Anders Alnor, et autres
Publié: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
par: Elad, Neta, et autres
Publié: (2025)