Cover Image

Complete first-order reasoning for functional programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Murali, Adithya, Peña, Lucas, Jhala, Ranjit, Madhusudan, P.
Format:	Preprint
Published:	2026
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

FO-Complete Program Verification for Heap Logics
by: Murali, Adithya, et al.
Published: (2026)

Predictable Verification using Intrinsic Definitions
by: Murali, Adithya, et al.
Published: (2024)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)

Verification Modulo Tested Library Contracts
by: Uppar, Abhishek, et al.
Published: (2026)

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

Multi types and reasonable space
by: Accattoli, Beniamino, et al.
Published: (2022)

TensorRocq: Enabling diagrammatic reasoning in Rocq
by: Caldwell, Benjamin, et al.
Published: (2026)

Complete and tractable machine-independent characterizations of second-order polytime
by: Hainry, Emmanuel, et al.
Published: (2022)

Expressivity of AuDaLa: Turing Completeness and Possible Extensions
by: Franken, Tom T. P., et al.
Published: (2024)

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

Checkpoint-based rollback recovery in session programming
by: Mezzina, Claudio Antares, et al.
Published: (2023)

A programming language characterizing quantum polynomial time
by: Hainry, Emmanuel, et al.
Published: (2022)

Complete Local Reasoning About Parameterized Programs Over Topologies
by: Cheng, Ruotong, et al.
Published: (2026)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
by: Stübinger, Terru, et al.
Published: (2023)

Higher-order bialgebraic semantics
by: Goncharov, Sergey, et al.
Published: (2024)

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

Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
by: Chatterjee, Krishnendu, et al.
Published: (2024)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
by: Hu, Jason Z. S., et al.
Published: (2024)

Making first order linear logic a generating grammar
by: Slavnov, Sergey
Published: (2022)

Proving Confluence in the Confluence Framework with CONFident
by: Gutiérrez, Raúl, et al.
Published: (2023)

Program Synthesis is $Σ_3^0$-Complete
by: Kim, Jinwoo
Published: (2024)

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
by: Ye, Kangfeng, et al.
Published: (2023)

On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
by: Matsuoka, Satoshi
Published: (2026)

Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
by: Ackerman, Nathanael L., et al.
Published: (2023)

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

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

Weighted GKAT: Completeness and Complexity
by: Van Koevering, Spencer, et al.
Published: (2025)

A programming language combining quantum and classical control
by: Dave, Kinnari, et al.
Published: (2025)

Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages
by: Carette, TItouan, et al.
Published: (2022)

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
by: Deng, Haotian, et al.
Published: (2025)

A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics
by: Ghica, Dan R., et al.
Published: (2022)

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

A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics
by: Barthe, Gilles, et al.
Published: (2025)

s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
by: Rao, Balaji, et al.
Published: (2026)

Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog
by: Amato, Gianluca, et al.
Published: (2024)

Sequential composition of answer set programs
by: Antić, Christian
Published: (2021)

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

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

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

Recursive Mutexes in Separation Logic
by: Du, Ke, et al.
Published: (2026)