Cover Image

Proving Confluence in the Confluence Framework with CONFident

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Gutiérrez, Raúl, Lucas, Salvador, Vítores, Miguel
Format:	Preprint
Published:	2023
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

Confluence of Conditional Rewriting Modulo
by: Lucas, Salvador
Published: (2025)

On Complexity Bounds and Confluence of Parallel Term Rewriting
by: Baudon, Thaïs, et al.
Published: (2023)

Compositional Confluence Criteria
by: Shintani, Kiraku, et al.
Published: (2023)

Confluence of Logically Constrained Rewrite Systems Revisited
by: Schöpf, Jonas, et al.
Published: (2024)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

Confluence Criteria for Logically Constrained Rewrite Systems (Full Version)
by: Schöpf, Jonas, et al.
Published: (2023)

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

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

Agentic Proving for Program Verification
by: Sosso, Alessandro, et al.
Published: (2026)

Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity
by: Chen, Hubie, et al.
Published: (2024)

An In-Context Learning Agent for Formal Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2023)

Complete first-order reasoning for functional programs
by: Murali, Adithya, et al.
Published: (2026)

Meaningfulness and Genericity in a Subsuming Framework
by: Kesner, Delia, et al.
Published: (2024)

DateSAT: A Framework for Solving Date and Period Constraints
by: Cui, Leyi, et al.
Published: (2026)

Automated Strategy Invention for Confluence of Term Rewrite Systems
by: Zhang, Liao, et al.
Published: (2024)

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
by: Li, Runming, et al.
Published: (2025)

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
by: Liu, Chengwu, et al.
Published: (2026)

Proceedings Twentieth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
by: Chaudhuri, Kaustuv, et al.
Published: (2025)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
by: Rustenholz, Louis, et al.
Published: (2024)

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

Proving and Computing: The Infinite Pigeonhole Principle and Countable Choice
by: Ariola, Zena M., et al.
Published: (2026)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
by: Liu, Qi, et al.
Published: (2025)

Proving Cutoff Bounds for Safety Properties in First-Order Logic
by: Lotan, Raz, et al.
Published: (2024)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Crash-Stop Failures in Asynchronous Multiparty Session Types
by: Barwell, Adam D., et al.
Published: (2023)

Types, equations, dimensions and the Pi theorem
by: Botta, Nicola, et al.
Published: (2023)

A flexible specification approach for verifying total correctness of fine-grained concurrent modules
by: Fasse, Justus, et al.
Published: (2023)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
by: Elad, Neta, et al.
Published: (2023)

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

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

Simply typed convertibility is TOWER-complete even for safe lambda-terms
by: Nguyên, Lê Thành Dũng
Published: (2023)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
by: Lahav, Ori, et al.
Published: (2023)

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

A denotationally-based program logic for higher-order store
by: Aagaard, Frederik Lerbjerg, et al.
Published: (2023)

Structural Analysis of GRAFCET Control Specifications
by: Schnakenbeck, Aron, et al.
Published: (2023)

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
by: Kappé, Tobias, et al.
Published: (2023)

A feasible and unitary quantum programming language
by: Díaz-Caro, Alejandro, et al.
Published: (2023)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
by: Klinkenberg, Lutz, et al.
Published: (2023)