Buchumschlag

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Foo, Darius, Song, Yahui, Chin, Wei-Ngan
Format:	Preprint
Veröffentlicht:	2023
Schlagworte:	Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Verified Parameterized Choreographies Technical Report
von: Rubbens, Robert, et al.
Veröffentlicht: (2025)

Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
von: Ciccalè, Marco, et al.
Veröffentlicht: (2025)

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)
von: Young, David, et al.
Veröffentlicht: (2024)

Leroy: Library Learning for Imperative Programming Languages
von: Bellur, Abhiram, et al.
Veröffentlicht: (2024)

SSA without Dominance for Higher-Order Programs
von: Leißa, Roland, et al.
Veröffentlicht: (2026)

Pleasant Imperative Program Proofs with GallinaC
von: Fort, Frédéric, et al.
Veröffentlicht: (2025)

Logical Predicates in Higher-Order Mathematical Operational Semantics
von: Goncharov, Sergey, et al.
Veröffentlicht: (2024)

Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
von: Nicola, Mihai, et al.
Veröffentlicht: (2024)

Verification Algorithms for Automated Separation Logic Verifiers
von: Eilers, Marco, et al.
Veröffentlicht: (2024)

Imperative vs. Declarative Programming Paradigms for Open-Universe Scene Generation
von: Gumin, Maxim, et al.
Veröffentlicht: (2025)

Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms
von: Alaoui, Ziad Ismaili, et al.
Veröffentlicht: (2025)

Imperative Quantum Programming with Ownership and Borrowing in Guppy
von: Koch, Mark, et al.
Veröffentlicht: (2025)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
von: Haselwarter, Philipp G., et al.
Veröffentlicht: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
von: Goncharov, Sergey, et al.
Veröffentlicht: (2024)

The Stable Model Semantics for Higher-Order Logic Programming
von: Bogaerts, Bart, et al.
Veröffentlicht: (2024)

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
von: Chirica, Ion, et al.
Veröffentlicht: (2025)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
von: Timany, Amin, et al.
Veröffentlicht: (2021)

From Program Logics to Language Logics
von: Cimini, Matteo
Veröffentlicht: (2024)

Formal Foundations for Translational Separation Logic Verifiers (extended version)
von: Dardinier, Thibault, et al.
Veröffentlicht: (2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
von: Haselwarter, Philipp G., et al.
Veröffentlicht: (2024)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
von: Wu, Jinhua, et al.
Veröffentlicht: (2025)

Creating Pleasant Programming Environments for Cognitive Science Students. Technical Report No. 16. [and] Domain Specific Debugging Aids for Novice Programmers. Technical Report No. 17.
von: Eisenstadt, Marc, et al.
Veröffentlicht: (1981)

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
von: Ling, Hongyi, et al.
Veröffentlicht: (2026)

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

Expanding Specification Capabilities of a Gradual Verifier with Pure Functions
von: Mutlu, Doruk Alp
Veröffentlicht: (2025)

Dependent Session Types for Verified Concurrent Programming
von: Fu, Qiancheng, et al.
Veröffentlicht: (2025)

Caesar: A Deductive Verifier for Probabilistic Programs
von: Schröer, Philipp, et al.
Veröffentlicht: (2026)

Implicit Rankings for Verifying Liveness Properties in First-Order Logic
von: Lotan, Raz, et al.
Veröffentlicht: (2024)

Fixed-Point-Oriented Programming: A Concise and Elegant Paradigm
von: Foo, Yong Qi, et al.
Veröffentlicht: (2025)

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

Functional Logic Program Transformations
von: Hanus, Michael, et al.
Veröffentlicht: (2026)

HITrees: Higher-Order Interaction Trees
von: Ayyam, Amir Mohammad Fadaei, et al.
Veröffentlicht: (2025)

Technical Report: Full-Stack Fine-Tuning for the Q Programming Language
von: Hogan, Brendan R., et al.
Veröffentlicht: (2025)

Higher Order Automatic Differentiation of Higher Order Functions
von: Huot, Mathieu, et al.
Veröffentlicht: (2021)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
von: Li, Kwing Hei, et al.
Veröffentlicht: (2025)

Minuska: Towards a Formally Verified Programming Language Framework
von: Tušil, Jan, et al.
Veröffentlicht: (2024)

Toward Verified Library-Level Choreographic Programming with Algebraic Effects
von: Shen, Gan, et al.
Veröffentlicht: (2024)

Qafny: A Quantum-Program Verifier
von: Li, Liyi, et al.
Veröffentlicht: (2022)

Higher-Order Behavioural Conformances via Fibrations
von: Urbat, Henning
Veröffentlicht: (2025)

Logical Relations for Formally Verified Authenticated Data Structures
von: Gregersen, Simon Oddershede, et al.
Veröffentlicht: (2025)