Buchumschlag

A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Affeldt, Reynald, Garrigue, Jacques, Saikawa, Takafumi
Format:	Preprint
Veröffentlicht:	2023
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Typed compositional quantum computation with lenses
von: Garrigue, Jacques, et al.
Veröffentlicht: (2023)

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
von: Affeldt, Reynald, et al.
Veröffentlicht: (2024)

A Foundation for Differentiable Logics using Dependent Type Theory
von: Affeldt, Reynald, et al.
Veröffentlicht: (2026)

The Formal Theory of Monads, Univalently
von: van der Weide, Niels
Veröffentlicht: (2022)

The Monadic Theory of Toric Words
von: Berthé, Valérie, et al.
Veröffentlicht: (2023)

Separability Properties of Monadically Dependent Graph Classes
von: Bonnet, Édouard, et al.
Veröffentlicht: (2025)

On the Decidability of Monadic Theories of Arithmetic Predicates
von: Berthé, Valérie, et al.
Veröffentlicht: (2024)

Taming Differentiable Logics with Coq Formalisation
von: Affeldt, Reynald, et al.
Veröffentlicht: (2024)

Flip-Breakability: A Combinatorial Dichotomy for Monadically Dependent Graph Classes
von: Dreier, Jan, et al.
Veröffentlicht: (2024)

Monadic Second-Order Logic of Permutations
von: Jelínek, Vít, et al.
Veröffentlicht: (2025)

Distributive Laws of Monadic Containers
von: Purdy, Chris, et al.
Veröffentlicht: (2025)

Graded Monads and Behavioural Equivalence Games
von: Ford, Chase, et al.
Veröffentlicht: (2022)

From Partial to Monadic: Combinatory Algebra with Effects
von: Cohen, Liron, et al.
Veröffentlicht: (2025)

A Graded Modal Dependent Type Theory with Erasure, Formalized
von: Abel, Andreas, et al.
Veröffentlicht: (2026)

Primitive Recursive Dependent Type Theory
von: Buchholtz, Ulrik, et al.
Veröffentlicht: (2024)

The Parameterized Complexity of Learning Monadic Second-Order Logic
von: van Bergerem, Steffen, et al.
Veröffentlicht: (2023)

Free Monads, Intrinsic Scoping, and Higher-Order Preunification
von: Kudasov, Nikolai
Veröffentlicht: (2022)

Representing Guardedness in Call-by-Value and Guarded Parametrized Monads
von: Goncharov, Sergey
Veröffentlicht: (2024)

The Unification Type of an Equational Theory May Depend on the Instantiation Preorder: From Results for Single Theories to Results for Classes of Theories
von: Baader, Franz, et al.
Veröffentlicht: (2026)

A Theory of Formal Choreographic Languages
von: Barbanera, Franco, et al.
Veröffentlicht: (2022)

Tape Diagrams for Monoidal Monads
von: Bonchi, Filippo, et al.
Veröffentlicht: (2025)

A topological reading of inductive and coinductive definitions in Dependent Type Theory
von: Sabelli, Pietro
Veröffentlicht: (2024)

Non-Derivability Results in Polymorphic Dependent Type Theory
von: Geuvers, Herman
Veröffentlicht: (2026)

Formalization of Amicable Numbers Theory
von: Chen, Zhipeng, et al.
Veröffentlicht: (2026)

What Monads Can and Cannot Do with a Few Extra Pages
von: Møgelberg, Rasmus Ejlers, et al.
Veröffentlicht: (2023)

The Only Distributive Law Over the Powerset Monad Is the One You Know
von: Goncharov, Sergey, et al.
Veröffentlicht: (2026)

Handling the Selection Monad (Full Version)
von: Plotkin, Gordon, et al.
Veröffentlicht: (2025)

Formalizing two-level type theory with cofibrant exo-nat
von: Uskuplu, Elif
Veröffentlicht: (2023)

Monadic Intersection Types, Relationally (Extended Version)
von: Gavazzo, Francesco, et al.
Veröffentlicht: (2024)

Stone Duality for Monads
von: Garner, Richard, et al.
Veröffentlicht: (2026)

Monads and Distributive Laws in Substructural Contexts (Extended Version)
von: Fujii, Soichiro, et al.
Veröffentlicht: (2026)

Smart Choices and the Selection Monad
von: Abadi, Martin, et al.
Veröffentlicht: (2020)

Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types
von: Mannucci, Mirco A., et al.
Veröffentlicht: (2026)

Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic
von: Díaz-Caro, Alejandro, et al.
Veröffentlicht: (2024)

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
von: Brough, Jackson
Veröffentlicht: (2026)

Datalog-Expressibility for Monadic and Guarded Second-Order Logic
von: Bodirsky, Manuel, et al.
Veröffentlicht: (2020)

Are Dependent Types in Set Theory Feasible?
von: Yang, Yunsong, et al.
Veröffentlicht: (2026)

A Formal Proof of Complexity Bounds on Diophantine Equations
von: Bayer, Jonas, et al.
Veröffentlicht: (2025)

Equational and Inductive Reasoning for Maude in Athena
von: Sanabria, Mateo, et al.
Veröffentlicht: (2026)

Practical Reasoning in DatalogMTL
von: Wang, Dingmin, et al.
Veröffentlicht: (2024)