Cover Image

Toward Verified Library-Level Choreographic Programming with Algebraic Effects

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Shen, Gan, Kuper, Lindsey
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Efficient, Portable, Census-Polymorphic Choreographic Programming
by: Bates, Mako, et al.
Published: (2024)

Freer Arrows and Why You Need Them in Haskell
by: VanDomelen, Grant, et al.
Published: (2025)

Inductive diagrams for causal reasoning
by: Castello, Jonathan, et al.
Published: (2023)

Accompanist: A Runtime for Resilient Choreographic Programming
by: Kløvedal, Viktor Strate, et al.
Published: (2026)

Efficient, Portable, Census-Polymorphic Choreographic Programming
by: Bates, Mako, et al.
Published: (2025)

Corps: A Core Calculus of Hierarchical Choreographic Programming
by: Hirsch, Andrew K.
Published: (2024)

A Promising Future: Omission Failures in Choreographic Programming
by: Graversen, Eva, et al.
Published: (2017)

Real-World Choreographic Programming: Full-Duplex Asynchrony and Interoperability
by: Lugović, Lovro, et al.
Published: (2023)

CRDT Emulation, Simulation, and Representation Independence
by: Liittschwager, Nathan, et al.
Published: (2025)

Towards a Function-as-a-Service Choreographic Programming Language: Examples and Applications
by: De Palma, Giuseppe, et al.
Published: (2024)

Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
by: Redmond, Patrick, et al.
Published: (2025)

Type-Based Enforcement of Non-Interference for Choreographic Programming
by: Bertoni, Marco, et al.
Published: (2026)

MultiChor: Census Polymorphic Choreographic Programming with Multiply Located Values
by: Bates, Mako, et al.
Published: (2024)

Minuska: Towards a Formally Verified Programming Language Framework
by: Tušil, Jan, et al.
Published: (2024)

Choreographic Quick Changes: First-Class Location (Set) Polymorphism
by: Samuelson, Ashley, et al.
Published: (2025)

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
by: Tekriwal, Mohit, et al.
Published: (2025)

Suki: Choreographed Distributed Dataflow in Rust
by: Laddad, Shadaj, et al.
Published: (2024)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
by: Fedchin, Aleksandr, et al.
Published: (2025)

We Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values
by: Bates, Mako, et al.
Published: (2024)

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

Dependent Session Types for Verified Concurrent Programming
by: Fu, Qiancheng, et al.
Published: (2025)

Caesar: A Deductive Verifier for Probabilistic Programs
by: Schröer, Philipp, et al.
Published: (2026)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
by: Parthasarathy, Gaurav, et al.
Published: (2024)

Towards Algebraic Subtyping for Extensible Records
by: Marques, Rodrigo, et al.
Published: (2024)

From Algebraic Word Problem to Program: A Formalized Approach
by: Wiemerslage, Adam, et al.
Published: (2020)

Pact: A Choreographic Language for Agentic Ecosystems
by: Gopinathan, Kiran, et al.
Published: (2026)

Remarks on Algebraic Reconstruction of Types and Effects
by: Balik, Patrycja, et al.
Published: (2026)

Signature Restriction for Polymorphic Algebraic Effects
by: Sekiyama, Taro, et al.
Published: (2020)

An Incremental Algorithm for Algebraic Program Analysis
by: Zhou, Chenyu, et al.
Published: (2024)

Qafny: A Quantum-Program Verifier
by: Li, Liyi, et al.
Published: (2022)

Modular Probabilistic Models via Algebraic Effects
by: Nguyen, Minh, et al.
Published: (2022)

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

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

LoRe: A Programming Model for Verifiably Safe Local-First Software
by: Haas, Julian, et al.
Published: (2023)

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

An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
by: Kammar, Ohad, et al.
Published: (2026)

GATlab: Modeling and Programming with Generalized Algebraic Theories
by: Lynch, Owen, et al.
Published: (2024)

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

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
by: de Vilhena, Paulo Emílio, et al.
Published: (2021)

Towards AI-Assisted Synthesis of Verified Dafny Methods
by: Misu, Md Rakib Hossain, et al.
Published: (2024)