On the public citation graph

Type-Checking CRDT Convergence

https://doi.org/10.1145/3591276
0 signed · 66 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/11554554_8openalex-snapshot
Cyclic Proofs for First-Order Logic with Inductive Definitions
inferredcites →https://doi.org/10.1007/11737414_9openalex-snapshot
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
inferredcites →https://doi.org/10.1007/3-540-36576-1_27openalex-snapshot
On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μCalculus
inferredcites →https://doi.org/10.1007/3-540-45949-9openalex-snapshot
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
inferredcites →https://doi.org/10.1007/3-540-60579-7_3openalex-snapshot
Codifying guarded definitions with recursive schemes
inferredcites →https://doi.org/10.1007/978-3-030-14805-8_4openalex-snapshot
Proving Type Class Laws for Haskell
inferredcites →https://doi.org/10.1007/978-3-030-25543-5_26openalex-snapshot
Automated Parameterized Verification of CRDTs
inferredcites →https://doi.org/10.1007/978-3-030-30048-7_35openalex-snapshot
Lemma Synthesis for Automating Induction over Algebraic Data Types
inferredcites →https://doi.org/10.1007/978-3-030-44914-8_20openalex-snapshot
Proving the Safety of Highly-Available Distributed Objects
inferredcites →https://doi.org/10.1007/978-3-030-53518-6_8openalex-snapshot
Induction with Generalization in Superposition Reasoning
inferredcites →https://doi.org/10.1007/978-3-030-81688-9_6openalex-snapshot
Theory Exploration Powered by Deductive Synthesis
inferredcites →https://doi.org/10.1007/978-3-030-99524-9_24openalex-snapshot
cvc5: A Versatile and Industrial-Strength SMT Solver
inferredcites →https://doi.org/10.1007/978-3-319-19890-3_55openalex-snapshot
Yjs: A Framework for Near Real-Time P2P Shared Editing on Arbitrary Data Types
inferredcites →https://doi.org/10.1007/978-3-319-20615-8_23openalex-snapshot
TIP: Tons of Inductive Problems
inferredcites →https://doi.org/10.1007/978-3-319-89960-2_7openalex-snapshot
Automatic Generation of Precise and Useful Commutativity Conditions
inferredcites →https://doi.org/10.1007/978-3-540-32254-2_12openalex-snapshot
History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!
inferredcites →https://doi.org/10.1007/978-3-540-78800-3_24openalex-snapshot
Z3: An Efficient SMT Solver
inferredcites →https://doi.org/10.1007/978-3-642-03359-9_6openalex-snapshot
A Brief Overview of Agda – A Functional Language with Dependent Types
inferredcites →https://doi.org/10.1007/978-3-642-13977-2_3openalex-snapshot
QuickSpec: Guessing Formal Specifications Using Testing
inferredcites →https://doi.org/10.1007/978-3-642-22110-1_14openalex-snapshot
CVC4
inferredcites →https://doi.org/10.1007/978-3-642-24550-3_29openalex-snapshot
Conflict-Free Replicated Data Types
inferredcites →https://doi.org/10.1007/978-3-642-28756-5_28openalex-snapshot
Zeno: An Automated Prover for Properties of Recursive Data Structures
inferredcites →https://doi.org/10.1007/978-3-642-35182-2_25openalex-snapshot
A Generic Cyclic Theorem Prover
inferredcites →https://doi.org/10.1007/978-3-662-43613-4_3openalex-snapshot
Formal Specification and Verification of CRDTs
inferredcites →https://doi.org/10.1007/978-3-662-46081-8_5openalex-snapshot
Induction for SMT Solvers
inferredcites →https://doi.org/10.1007/s10489-017-0954-8openalex-snapshot
MATHsAiD: Automated mathematical theory exploration
inferredcites →https://doi.org/10.1016/0898-1221(94)00215-7openalex-snapshot
The Boyer-Moore theorem prover and its interactive enhancement
inferredcites →https://doi.org/10.1016/b978-044450813-3/50016-3openalex-snapshot
Inductionless Induction
inferredcites →https://doi.org/10.1016/j.jpdc.2017.08.003openalex-snapshot
Delta state replicated data types
inferredcites →https://doi.org/10.1017/s0960129503004122openalex-snapshot
Type-based termination of recursive definitions
inferredcites →https://doi.org/10.1109/32.713327openalex-snapshot
Subtypes for specifications: predicate subtyping in PVS
inferredcites →https://doi.org/10.1109/jsac.2002.806121openalex-snapshot
Language-based information-flow security
inferredcites →https://doi.org/10.1109/tpds.2017.2697382openalex-snapshot
A Conflict-Free Replicated JSON Datatype
inferredcites →https://doi.org/10.1145/1435417.1435432openalex-snapshot
Eventually consistent
inferredcites →https://doi.org/10.1145/1508244.1508273openalex-snapshot
Commutativity analysis for software parallelization
inferredcites →https://doi.org/10.1145/2628136.2628161openalex-snapshot
Refinement types for Haskell
inferredcites →https://doi.org/10.1145/268946.268976openalex-snapshot
The SLam calculus
inferredcites →https://doi.org/10.1145/277650.277732openalex-snapshot
Eliminating array bound checking through dependent types
inferredcites →https://doi.org/10.1145/277830.277870openalex-snapshot
The role of associativity and commutativity in the detection and transformation of loop-level parallelism
inferredcites →https://doi.org/10.1145/3133956.3133998openalex-snapshot
A Type System for Privacy Properties
inferredcites →https://doi.org/10.1145/3158141openalex-snapshot
Refinement reflection: complete verification with SMT
inferredcites →https://doi.org/10.1145/3380787.3393687openalex-snapshot
Composing and decomposing op-based CRDTs with semidirect products
inferredcites →https://doi.org/10.1145/3428284openalex-snapshot
Verifying replicated data types with typeclass refinements in Liquid Haskell
inferredcites →https://doi.org/10.1145/351240.351266openalex-snapshot
QuickCheck
inferredcites →https://doi.org/10.1145/3519939.3523731openalex-snapshot
CycleQ: an efficient basis for cyclic equational reasoning
inferredcites →https://doi.org/10.1145/3563336openalex-snapshot
Katara: synthesizing CRDTs with verified lifting
inferredcites →https://doi.org/10.1145/67544.66963openalex-snapshot
Concurrency control in groupware systems
inferredcites →https://doi.org/10.1145/800194.805852openalex-snapshot
Definitional interpreters for higher-order programming languages
inferredcites →https://doi.org/10.29007/3qwropenalex-snapshot
HipSpec : Automating Inductive Proofs of Program Properties
inferredcites →https://doi.org/10.5281/zenodo.7674926openalex-snapshot
Type-Checking CRDT Convergence

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1002/spe.3430openalex-snapshot
Concurrency Contracts for Designing Highly Available Replicated Data Types
inferred← citeshttps://doi.org/10.1109/access.2025.3568925openalex-snapshot
Crust: A Modular Framework for Conflict-Free Replicated Data Types (CRDTs) Development, Validation, and Benchmarking
inferred← citeshttps://doi.org/10.1109/nrsc71102.2026.11556041openalex-snapshot
EC-VDIC: A Scalable and Verifiable Adaptive Erasure Coding Framework for Decentralized IPFS Clusters
inferred← citeshttps://doi.org/10.1109/tse.2024.3393070openalex-snapshot
Automated Infrastructure as Code Program Testing
inferred← citeshttps://doi.org/10.1109/tse.2024.3477723openalex-snapshot
Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications
inferred← citeshttps://doi.org/10.1145/3618305.3623610openalex-snapshot
Safe Combination of Data-Centric and Operation-Centric Consistency
inferred← citeshttps://doi.org/10.1145/3633769openalex-snapshot
LoRe: A Programming Model for Verifiably Safe Local-first Software
inferred← citeshttps://doi.org/10.1145/3656408openalex-snapshot
Automated Verification of Fundamental Algebraic Laws
inferred← citeshttps://doi.org/10.1145/3704913openalex-snapshot
Dis/Equality Graphs
inferred← citeshttps://doi.org/10.1145/3720425openalex-snapshot
Hambazi: Spatial Coordination Synthesis for Augmented Reality
inferred← citeshttps://doi.org/10.1145/3720502openalex-snapshot
Bolt-On Strong Consistency: Specification, Implementation, and Verification
inferred← citeshttps://doi.org/10.1145/3720513openalex-snapshot
Peepco: Batch-Based Consistency Optimization
inferred← citeshttps://doi.org/10.1145/3808249openalex-snapshot
Versioned E-Graphs
inferred← citeshttps://doi.org/10.1145/3839478openalex-snapshot
Composing CRDTs Convergent by Construction
inferred← citeshttps://doi.org/10.62660/bcstu/1.2024openalex-snapshot
inferred← citeshttps://doi.org/10.62660/bcstu/1.2024.23openalex-snapshot
Performance optimisation techniques for Conflict-free Replicated Data Types (CRDT)
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.