Image de couverture de livre

Expanding Specification Capabilities of a Gradual Verifier with Pure Functions

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteur principal:	Mutlu, Doruk Alp
Format:	Preprint
Publié:	2025
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

Increasing the Expressiveness of a Gradual Verifier
par: Gupta, Priyam
Publié: (2025)

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

Verifying Properties of Index Arrays in a Purely-Functional Data-Parallel Language
par: Hinnerskov, Nikolaj Hey, et autres
Publié: (2025)

Gradual Sensitivity Typing
par: Arquez, Damian, et autres
Publié: (2023)

Compiling Gradual Types with Evidence
par: Romero, José Luis, et autres
Publié: (2025)

Gradual Metaprogramming
par: Chen, Tianyu, et autres
Publié: (2025)

A Gradual Probabilistic Lambda Calculus
par: Ye, Wenjia, et autres
Publié: (2026)

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
par: Foo, Darius, et autres
Publié: (2023)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
par: Zimmerman, Conrad, et autres
Publié: (2024)

Efficient Selection of Type Annotations for Performance Improvement in Gradual Typing
par: Li, Senxi, et autres
Publié: (2026)

Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings
par: Bagrel, Thomas
Publié: (2026)

Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes
par: Bagrel, Thomas, et autres
Publié: (2025)

Taming Scope Extrusion in Gradual Imperative Metaprogramming
par: Chen, Tianyu, et autres
Publié: (2026)

Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version)
par: Giovannini, Eric, et autres
Publié: (2024)

Gradual Verification for Smart Contracts
par: Sun, Haojia, et autres
Publié: (2023)

Dynamic Program Slices Change How Developers Diagnose Gradual Run-Time Type Errors
par: Schwerter, Felipe Bañados, et autres
Publié: (2025)

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
par: Wu, Jinhua, et autres
Publié: (2026)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
par: Wu, Jinhua, et autres
Publié: (2025)

Verifying Functional Correctness Properties At the Level of Java Bytecode
par: Paganoni, Marco, et autres
Publié: (2024)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
par: Castagna, Giuseppe, et autres
Publié: (2024)

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

Verified Code Transpilation with LLMs
par: Bhatia, Sahil, et autres
Publié: (2024)

Quest Complete: the Holy Grail of Gradual Security
par: Chen, Tianyu, et autres
Publié: (2023)

Crux, a Precise Verifier for Rust and Other Languages
par: Pernsteiner, Stuart, et autres
Publié: (2024)

Verified Parameterized Choreographies Technical Report
par: Rubbens, Robert, et autres
Publié: (2025)

Pyrosome: Verified Compilation for Modular Metatheory
par: Jamner, Dustin, et autres
Publié: (2025)

Automatically Verifying Replication-aware Linearizability
par: Soundarapandian, Vimala, et autres
Publié: (2025)

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
par: Pezeshkpour, Pouya, et autres
Publié: (2026)

Minuska: Towards a Formally Verified Programming Language Framework
par: Tušil, Jan, et autres
Publié: (2024)

A Pure Demand Operational Semantics with Applications to Program Analysis
par: Smith, Scott, et autres
Publié: (2023)

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
par: Matsushita, Yusuke, et autres
Publié: (2026)

Dependent Session Types for Verified Concurrent Programming
par: Fu, Qiancheng, et autres
Publié: (2025)

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

Verifying Sequential Consistency under Bounded Preemptions
par: Govind, R., et autres
Publié: (2026)

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation
par: Yang, Xiaoxiao, et autres
Publié: (2017)

Caesar: A Deductive Verifier for Probabilistic Programs
par: Schröer, Philipp, et autres
Publié: (2026)

KATch: A Fast Symbolic Verifier for NetKAT
par: Moeller, Mark, et autres
Publié: (2024)

Rows and Capabilities as Modal Effects
par: Tang, Wenhao, et autres
Publié: (2025)

Typestate via Revocable Capabilities
par: Jia, Songlin, et autres
Publié: (2025)

Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language
par: Pedersen, Jan, et autres
Publié: (2025)