:: Library Catalog

Image de couverture de livre

Enregistré dans:

Détails bibliographiques
Auteur principal:	Kappelmann, Kevin
Format:	Preprint
Publié:	2025
Sujets:	Logic in Computer Science Programming Languages
Accès en ligne:	https://arxiv.org/abs/2503.20413
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Transport via Partial Galois Connections and Equivalences
par: Kappelmann, Kevin
Publié: (2023)

Coinductive Proofs for Temporal Hyperliveness
par: Correnson, Arthur, et autres
Publié: (2025)

Symmetric Proofs of Parameterized Programs
par: Cheng, Ruotong, et autres
Publié: (2026)

More Church-Rosser Proofs in BELUGA
par: Momigliano, Alberto, et autres
Publié: (2024)

Cyclic Proofs in Hoare Logic and its Reverse
par: Brotherston, James, et autres
Publié: (2025)

Pleasant Imperative Program Proofs with GallinaC
par: Fort, Frédéric, et autres
Publié: (2025)

Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model
par: Kappelmann, Kevin, et autres
Publié: (2025)

Mechanised Hypersafety Proofs about Structured Data: Extended Version
par: Gladshtein, Vladimir, et autres
Publié: (2024)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
par: Oda, Yukihiro
Publié: (2025)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
par: Vollmer, Victoria, et autres
Publié: (2024)

Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report)
par: Rowicki, Radosław Jan, et autres
Publié: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
par: Elad, Neta, et autres
Publié: (2025)

Verifying Lock-free Search Structure Templates
par: Patel, Nisarg, et autres
Publié: (2024)

An Introduction to Razborov's Flag Algebra as a Proof System for Extremal Graph Theory
par: Jeong, Gyeongwon, et autres
Publié: (2026)

A Proof-Producing Compiler for Blockchain Applications
par: Avigad, Jeremy, et autres
Publié: (2025)

A Deductive System for Contract Satisfaction Proofs
par: Correnson, Arthur, et autres
Publié: (2026)

Quantifier Elimination and Craig Interpolation, Quantitatively
par: Batz, Kevin, et autres
Publié: (2025)

Towards a Certified Proof Checker for Deep Neural Network Verification
par: Desmartin, Remi, et autres
Publié: (2023)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
par: Desmartin, Remi, et autres
Publié: (2024)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
par: Viennot, Jules, et autres
Publié: (2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
par: Batz, Kevin, et autres
Publié: (2025)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
par: Batz, Kevin, et autres
Publié: (2024)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
par: Thakur, Amitayush, et autres
Publié: (2025)

Meaningfulness and Genericity in a Subsuming Framework
par: Kesner, Delia, et autres
Publié: (2024)

GATlab: Modeling and Programming with Generalized Algebraic Theories
par: Lynch, Owen, et autres
Publié: (2024)

Kleene algebra with commutativity conditions is undecidable
par: de Amorim, Arthur Azevedo, et autres
Publié: (2024)

CIll: CTI-Guided Invariant Generation via LLMs for Model Checking
par: Su, Yuheng, et autres
Publié: (2026)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
par: Klinkenberg, Lutz, et autres
Publié: (2023)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
par: Stübinger, Terru, et autres
Publié: (2023)

Cypher is Turing-Complete: A Formal Proof via 2-Counter Machine Simulation
par: Halftermeyer, Pierre
Publié: (2026)

Can Proof Assistants Verify Multi-Agent Systems?
par: Mendez, Julian Alfredo, et autres
Publié: (2025)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
par: Kaye, George
Publié: (2025)

Impredicativity in Linear Dependent Type Theory
par: Speight, Sam, et autres
Publié: (2026)

A Probabilistic Choreography Language for PRISM
par: Carbone, Marco, et autres
Publié: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
par: Zilberstein, Noam, et autres
Publié: (2025)

Positive Sharing and Abstract Machines
par: Accattoli, Beniamino, et autres
Publié: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
par: Grandury, Marcos, et autres
Publié: (2025)

Expressive Power of One-Shot Control Operators and Coroutines
par: Kobayashi, Kentaro, et autres
Publié: (2025)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
par: Ukhanov, Evgeny
Publié: (2025)

The Functional Machine Calculus III: Control
par: Heijltjes, Willem
Publié: (2025)