:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Momigliano, Alberto, Sassella, Martina
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Programming Languages
Online Access:	https://arxiv.org/abs/2404.14921
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Property-Based Testing by Elaborating Proof Outlines
by: Miller, Dale, et al.
Published: (2024)

A Beluga Formalization of the Harmony Lemma in the $π$-Calculus
by: Cecilia, Gabriele, et al.
Published: (2024)

Symmetric Proofs of Parameterized Programs
by: Cheng, Ruotong, et al.
Published: (2026)

Coinductive Proofs for Temporal Hyperliveness
by: Correnson, Arthur, et al.
Published: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

Pleasant Imperative Program Proofs with GallinaC
by: Fort, Frédéric, et al.
Published: (2025)

Zippy -- Generic White-Box Proof Search with Zippers
by: Kappelmann, Kevin
Published: (2025)

Mechanised Hypersafety Proofs about Structured Data: Extended Version
by: Gladshtein, Vladimir, et al.
Published: (2024)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
by: Vollmer, Victoria, et al.
Published: (2024)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
by: Oda, Yukihiro
Published: (2025)

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)

An Introduction to Razborov's Flag Algebra as a Proof System for Extremal Graph Theory
by: Jeong, Gyeongwon, et al.
Published: (2026)

A Deductive System for Contract Satisfaction Proofs
by: Correnson, Arthur, et al.
Published: (2026)

A Proof-Producing Compiler for Blockchain Applications
by: Avigad, Jeremy, et al.
Published: (2025)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
by: Desmartin, Remi, et al.
Published: (2024)

Towards a Certified Proof Checker for Deep Neural Network Verification
by: Desmartin, Remi, et al.
Published: (2023)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
by: Viennot, Jules, et al.
Published: (2025)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

Catamorphic Abstractions for Constrained Horn Clause Satisfiability
by: De Angelis, Emanuele, et al.
Published: (2024)

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

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

Can Proof Assistants Verify Multi-Agent Systems?
by: Mendez, Julian Alfredo, et al.
Published: (2025)

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)

Structural Temporal Logic for Mechanized Program Verification
by: Ioannidis, Eleftherios, et al.
Published: (2024)

An Introduction to Different Approaches to Initial Semantics
by: Lamiaux, Thomas, et al.
Published: (2024)

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

A Nominal Approach to Probabilistic Separation Logic
by: Li, John M., et al.
Published: (2024)

Syntax-Guided Automated Program Repair for Hyperproperties
by: Beutner, Raven, et al.
Published: (2024)

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

Hybrid Intersection Types for PCF (Extended Version)
by: Barenbaum, Pablo, et al.
Published: (2024)

Verifying Lock-free Search Structure Templates
by: Patel, Nisarg, et al.
Published: (2024)

Functional Array Programming in an Extended Pi-Calculus
by: Hüttel, Hans, et al.
Published: (2024)

An Abstract Domain for Heap Commutativity (Extended Version)
by: Pincus, Jared, et al.
Published: (2024)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
by: Verscht, Lena, et al.
Published: (2024)

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

Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming
by: Jang, Junyoung, et al.
Published: (2024)

The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)
by: Accattoli, Beniamino
Published: (2024)

Useful Evaluation: Syntax and Semantics (Technical Report)
by: Barenbaum, Pablo, et al.
Published: (2024)

Linear Contextual Metaprogramming and Session Types
by: Ângelo, Pedro, et al.
Published: (2024)