Cover Image

Complex Bounded Operators in Isabelle/HOL

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Unruh, Dominique, Caballero, José Manuel Rodríguez
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Brownian Motion in Isabelle/HOL
by: Laursen, Christian Pardillo, et al.
Published: (2024)

Linear Programming in Isabelle/HOL
by: Parsert, Julian
Published: (2024)

Verifying Numerical Methods with Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2025)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
by: Bartl, Lukas, et al.
Published: (2025)

Stalnaker's Epistemic Logic in Isabelle/HOL
by: Guzman, Laura P. Gamboa, et al.
Published: (2024)

Formalization of Differential Privacy in Isabelle/HOL
by: Sato, Tetsuya, et al.
Published: (2024)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
by: Foster, Simon, et al.
Published: (2024)

L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
by: Linzi, Alessandro
Published: (2025)

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
by: Hulak, David B., et al.
Published: (2026)

Munkres' General Topology Autoformalized in Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2026)

Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
by: Munive, Jonathan Julián Huerta y, et al.
Published: (2024)

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

A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL
by: Schmoetten, Richard, et al.
Published: (2024)

Quantum references
by: Unruh, Dominique
Published: (2021)

Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
by: Binder, Sage, et al.
Published: (2026)

Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL
by: Kim, Jinwook
Published: (2026)

Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library
by: Bilotta, Antonella
Published: (2025)

Bayesian Inference in Quantum Programs
by: Gehnen, Christina, et al.
Published: (2025)

Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)

Proof Recommendation System for the HOL4 Theorem Prover
by: Dekhil, Nour, et al.
Published: (2024)

Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
by: Huch, Fabian
Published: (2024)

Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security
by: Kammüller, Florian
Published: (2023)

Mechanized HOL Reasoning in Set Theory
by: Guilloud, Simon, et al.
Published: (2024)

On the Formalization of Network Topology Matrices in HOL
by: Aksoy, Kubra, et al.
Published: (2026)

On proving consistency of equational theories in Bounded Arithmetic
by: Beckmann, Arnold, et al.
Published: (2022)

Wadge degrees of $Δ^0_2$ omega-powers
by: Finkel, Olivier, et al.
Published: (2024)

A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
by: Melani, Beatrice, et al.
Published: (2025)

Cyclic Implicit Complexity
by: Curzi, Gianluca, et al.
Published: (2021)

Type Inference for Isabelle2Cpp
by: Jiang, Dongchen, et al.
Published: (2024)

The Complexity of the Constructive Master Modality
by: Santiago-Fernández, Sofía, et al.
Published: (2026)

Quasi Directed Jonsson Operations Imply Bounded Width (For fo-expansions of symmetric binary cores with free amalgamation)
by: Wrona, Michal
Published: (2024)

First-order Logic with Being a Thesis Modal Operator
by: Łyczak, Marcin
Published: (2024)

Lower Bounds on Inverse Cellular Automata via Proof Complexity
by: Kapytka, Maryia
Published: (2026)

Hyperarithmetical Complexity of Infinitary Action Logic with Multiplexing
by: Pshenitsyn, Tikhon
Published: (2023)

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

Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat
by: Tóth, Jan, et al.
Published: (2024)

Transpension: The Right Adjoint to the Pi-type
by: Nuyts, Andreas, et al.
Published: (2020)

Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
by: Mannucci, Mirco A., et al.
Published: (2025)

Complexity of the Model Checking problem for inquisitive propositional and modal logic
by: Grilletti, Gianluca, et al.
Published: (2024)