Cover Image

Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Ciccalè, Marco, Jurjo-Rivas, Daniel, Morales, Jose F., López-García, Pedro, Hermenegildo, Manuel V.
Format:	Preprint
Published:	2025
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Exploiting Multiple Abstract Call Patterns for Optimizing Run-Time Checks
by: Ferreiro, Daniela, et al.
Published: (2026)

Abstract Environment Trimming
by: Jurjo-Rivas, Daniel, 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)

Checkification: A Practical Approach for Testing Static Analysis Truths
by: Ferreiro, Daniela, et al.
Published: (2025)

Abstractions of Sequences, Functions and Operators
by: Rustenholz, Louis, et al.
Published: (2025)

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

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)
by: Young, David, et al.
Published: (2024)

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
by: Foo, Darius, et al.
Published: (2023)

SSA without Dominance for Higher-Order Programs
by: Leißa, Roland, et al.
Published: (2026)

Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs
by: Xu, Han, et al.
Published: (2026)

Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
by: Nicola, Mihai, et al.
Published: (2024)

C*: Unifying Programming and Verification in C
by: Cao, Yiyuan, et al.
Published: (2025)

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
by: Faella, Marco, et al.
Published: (2024)

Towards Automated Verification of LLM-Synthesized C Programs
by: Mukherjee, Prasita, et al.
Published: (2024)

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)

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

Practical Formal Verification for MLIR Programs
by: Tucker, Emily, et al.
Published: (2026)

HITrees: Higher-Order Interaction Trees
by: Ayyam, Amir Mohammad Fadaei, et al.
Published: (2025)

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

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

Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
by: Nagar, Kartik, et al.
Published: (2020)

Solvable Tuple Patterns and Their Applications to Program Verification
by: Kobayashi, Naoki, et al.
Published: (2025)

Higher-Order Behavioural Conformances via Fibrations
by: Urbat, Henning
Published: (2025)

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

ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses
by: Singh, Avaljot, et al.
Published: (2024)

Resource Specifications for Resource-Manipulating Programs
by: Grannan, Zachary, et al.
Published: (2023)

Actegories, Copowers, and Higher-Order Message Passing Semantics
by: Cockett, Robin, et al.
Published: (2025)

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

A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs
by: Rustenholz, Louis, et al.
Published: (2024)

QCP: A Practical Separation Logic-based C Program Verification Tool
by: Wu, Xiwei, et al.
Published: (2025)

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
by: Dane, Serra Z., et al.
Published: (2026)

Composing Automatic Differentiation with Custom Derivatives of Higher-Order Functions
by: Estep, Sam
Published: (2024)

Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
by: Yang, Zhixuan, et al.
Published: (2025)

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

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

KestRel: Relational Verification Using E-Graphs for Program Alignment
by: Dickerson, Robert, et al.
Published: (2024)

Weighted NetKAT: A Programming Language For Quantitative Network Verification
by: Acevedo, Emmanuel Suárez, et al.
Published: (2026)

Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report
by: Giunti, Marco, et al.
Published: (2025)

A Hybrid Approach to Semi-automated Rust Verification
by: Ayoun, Sacha-Élie, et al.
Published: (2024)