Imagen de Portada

Tail Modulo Cons, OCaml, and Relational Separation Logic

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Allain, Clément, Bour, Frédéric, Clément, Basile, Pottier, François, Scherer, Gabriel
Formato:	Preprint
Publicado:	2024
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

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

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

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

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

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

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

Context-Aware Separation Logic
por: Meyer, Roland, et al.
Publicado: (2023)

Hyper Separation Logic (extended version)
por: Gospodinov, Trayan, et al.
Publicado: (2026)

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

Automatic layout of railroad diagrams
por: Chiplunkar, Shardul, et al.
Publicado: (2025)

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

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

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

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

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

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

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

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

Recursive Mutexes in Separation Logic
por: Du, Ke, et al.
Publicado: (2026)

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

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

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

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

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

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

Towards Concurrent Quantitative Separation Logic
por: Fesefeldt, Ira, et al.
Publicado: (2022)

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

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

Agentic Separation Logic Specification Synthesis
por: Suresh, Tarun, et al.
Publicado: (2026)

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

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

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

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

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

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

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

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

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

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