Cover Image

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	de Vilhena, Paulo Emílio, Pottier, François
Format:	Preprint
Published:	2021
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers
by: Endo, Ryunosuke, et al.
Published: (2025)

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
by: Poli, Federico, et al.
Published: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

Verifying Floating-Point Programs in Stainless
by: Gilot, Andrea, et al.
Published: (2026)

Verifying Lock-free Search Structure Templates
by: Patel, Nisarg, et al.
Published: (2024)

Verifying Solutions to Semantics-Guided Synthesis Problems
by: Murphy, Charlie, et al.
Published: (2024)

Verifying Peephole Rewriting In SSA Compiler IRs
by: Bhat, Siddharth, et al.
Published: (2024)

Verifying Functional Correctness Properties At the Level of Java Bytecode
by: Paganoni, Marco, et al.
Published: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

revTPL: The Reversible Temporal Process Language
by: Bocchi, Laura, et al.
Published: (2022)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Reversible Computation with Stacks and "Reversible Management of Failures"
by: Palazzo, Matteo, et al.
Published: (2025)

The Semantics of Effects: Centrality, Quantum Control and Reversible Recursion
by: Lemonnier, Louis
Published: (2024)

A Constraint-based Mathematical Modeling Library in Prolog with Answer Constraint Semantics
by: Fages, François
Published: (2024)

Semantic Properties of Computations Defined by Elementary Inference Systems
by: Lucas, Salvador
Published: (2025)

Verification of Recursively Defined Quantum Circuits
by: Ying, Mingsheng, et al.
Published: (2024)

CSLib: The Lean Computer Science Library
by: Barrett, Clark, et al.
Published: (2026)

Verifying Asynchronous Hyperproperties in Reactive Systems
by: Beutner, Raven, et al.
Published: (2025)

A Reversible Semantics for Janus
by: Lanese, Ivan, et al.
Published: (2026)

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

Strong Normalisation for Asynchronous Effects
by: Ahman, Danel, et al.
Published: (2026)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
by: Ileri, Atalay Mert, et al.
Published: (2024)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
by: Montesi, Fabrizio, et al.
Published: (2026)

Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
by: Henson, Christopher, et al.
Published: (2026)

Type-Based Termination for Futures
by: Somayyajula, Siva, et al.
Published: (2021)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
by: Zilberstein, Noam, et al.
Published: (2023)

Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
by: Zilberstein, Noam
Published: (2024)

On Complete Categorical Semantics for Effect Handlers
by: Kura, Satoshi
Published: (2026)

An Intermediate Program Representation for Optimizing Stream-Based Languages
by: Baumeister, Jan, et al.
Published: (2025)

Equational Bit-Vector Solving via Strong Gröbner Bases
by: Song, Jiaxin, et al.
Published: (2024)

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

Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
by: Sulzmann, Martin
Published: (2026)

Denotational Foundations for Expected Cost Analysis
by: de Amorim, Pedro H. Azevedo
Published: (2024)

Domain Reasoning in TopKAT
by: Zhang, Cheng, et al.
Published: (2024)