Cover Image

Intrinsically Correct Algorithms and Recursive Coalgebras

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Alexandru, Cass, Urbat, Henning, Wißmann, Thorsten
Format:	Preprint
Published:	2025
Subjects:	Programming Languages Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Well-Founded Coalgebras Meet König's Lemma
by: Urbat, Henning, et al.
Published: (2025)

Abstract Operational Methods for Call-by-Push-Value
by: Goncharov, Sergey, et al.
Published: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
by: Goncharov, Sergey, et al.
Published: (2024)

Bialgebraic Reasoning on Stateful Languages
by: Goncharov, Sergey, et al.
Published: (2025)

Logical Predicates in Higher-Order Mathematical Operational Semantics
by: Goncharov, Sergey, et al.
Published: (2024)

Towards a Higher-Order Bialgebraic Denotational Semantics
by: Goncharov, Sergey, et al.
Published: (2026)

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

Trees in Coalgebra from Generalized Reachability
by: Wißmann, Thorsten, et al.
Published: (2025)

Efficient Coalgebraic Partition Refinement
by: Dorsch, Ulrich, et al.
Published: (2017)

Towards a Higher-Order Mathematical Operational Semantics
by: Goncharov, Sergey, et al.
Published: (2022)

Compositionality in Coalgebraic Trace Semantics
by: Jourde, Robin, et al.
Published: (2026)

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

Products of Recursive Programs for Hypersafety Verification (Extended Version)
by: Cheng, Ruotong, et al.
Published: (2025)

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

Coalgebraic Non-Wellfounded Proofs: Recursiveness and GTC
by: Kori, Mayuko
Published: (2026)

Initial Algebras Unchained -- A Novel Initial Algebra Construction Formalized in Agda
by: Wißmann, Thorsten, et al.
Published: (2024)

Coalgebraic Behavioral Metrics
by: Baldan, Paolo, et al.
Published: (2017)

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

Non-Cartesian Guarded Recursion with Daggers
by: Lemonnier, Louis
Published: (2024)

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

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

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
by: Lööw, Andreas, et al.
Published: (2024)

Algebraic Reasoning over Relational Structures
by: Jurka, Jan, et al.
Published: (2024)

A Unified Treatment of Substitution for Presheaves, Nominal Sets, Renaming Sets, and so on
by: Lenke, Fabian, et al.
Published: (2026)

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

An Expressive Coalgebraic Modal Logic for Cellular Automata
by: Basold, Henning, et al.
Published: (2025)

Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report)
by: Rowicki, Radosław Jan, et al.
Published: (2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
by: Tsukada, Takeshi, et al.
Published: (2025)

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

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

Intrinsically Correct Sorting in Cubical Agda
by: Alexandru, Cass, et al.
Published: (2024)

Flexible Correct-by-Construction Programming
by: Runge, Tobias, et al.
Published: (2022)

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

A Coalgebraic Semantics for Intuitionistic Modal Logic
by: Almeida, Rodrigo Nicolau, et al.
Published: (2024)

Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion
by: Zhang, Dylan, et al.
Published: (2024)

Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi
by: Cerda, Rémy
Published: (2025)

Coalgebraic Path Constraints
by: Schmid, Todd
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)

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)