Cover Image

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Chirica, Ion, Pereira, Mário
Format:	Preprint
Published:	2025
Subjects:	Programming Languages Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)
by: Soares, Tiago Lopes, et al.
Published: (2024)

Practical Deductive Verification of OCaml Programs (Extended Version)
by: Pereira, Mário
Published: (2024)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
by: Haselwarter, Philipp G., et al.
Published: (2026)

Higher Order Automatic Differentiation of Higher Order Functions
by: Huot, Mathieu, et al.
Published: (2021)

Higher-Order Asynchronous Effects
by: Ahman, Danel, et al.
Published: (2023)

Bialgebraic Reasoning on Higher-Order Program Equivalence
by: Goncharov, Sergey, et al.
Published: (2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Logical Predicates in Higher-Order Mathematical Operational Semantics
by: Goncharov, Sergey, et al.
Published: (2024)

Towards a Higher-Order Bialgebraic Denotational Semantics
by: Goncharov, Sergey, et al.
Published: (2026)

On Higher-Order Reachability Games vs May Reachability
by: Asada, Kazuyuki, et al.
Published: (2022)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
by: Timany, Amin, et al.
Published: (2021)

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
by: Chen, Zhibo, et al.
Published: (2023)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
by: Aguirre, Alejandro, et al.
Published: (2024)

The Power of Negation in Higher-Order Datalog
by: Charalambidis, Angelos, et al.
Published: (2025)

Automated Software Verification of Hyperliveness
by: Beutner, Raven
Published: (2024)

Towards a Higher-Order Mathematical Operational Semantics
by: Goncharov, Sergey, et al.
Published: (2022)

Predictable Verification using Intrinsic Definitions
by: Murali, Adithya, et al.
Published: (2024)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

Structural Temporal Logic for Mechanized Program Verification
by: Ioannidis, Eleftherios, et al.
Published: (2024)

FO-Complete Program Verification for Heap Logics
by: Murali, Adithya, et al.
Published: (2026)

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

Products of Recursive Programs for Hypersafety Verification (Extended Version)
by: Cheng, Ruotong, et al.
Published: (2025)

Automated Verification of Monotonic Data Structure Traversals in C
by: Sotoudeh, Matthew
Published: (2025)

From Time to Space: The Impact of Linearity in Higher-Order Datalog
by: Charalambidis, Angelos, et al.
Published: (2026)

Higher-order bialgebraic semantics
by: Goncharov, Sergey, et al.
Published: (2024)

HaliVer: Deductive Verification and Scheduling Languages Join Forces
by: Haak, Lars B. van den, et al.
Published: (2024)

Structural Analysis of GRAFCET Control Specifications
by: Schnakenbeck, Aron, et al.
Published: (2023)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
by: Tsukada, Takeshi, et al.
Published: (2025)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
by: Batz, Kevin, et al.
Published: (2025)

Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
by: Chatterjee, Krishnendu, et al.
Published: (2024)

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
by: Cristiá, Maximiliano, et al.
Published: (2022)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
by: Elad, Neta, et al.
Published: (2023)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
by: Zimmerman, Conrad, et al.
Published: (2024)

Boosting Few-Pixel Robustness Verification via Covering Verification Designs
by: Shapira, Yuval, et al.
Published: (2024)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
by: Rustenholz, Louis, et al.
Published: (2024)

Gradual Verification for Smart Contracts
by: Sun, Haojia, et al.
Published: (2023)

Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation
by: Gros, Charlène, et al.
Published: (2024)