:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Author:	Carneiro, Mario
Format:	Preprint
Published:	2024
Subjects:	Programming Languages F.4.1; G.4; D.2.4
Online Access:	https://arxiv.org/abs/2403.14064
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Reimplementing Mizar in Rust
by: Carneiro, Mario
Published: (2023)

LeanLTL: A unifying framework for linear temporal logics in Lean
by: Vin, Eric, et al.
Published: (2025)

Ground Stratification for a Logic of Definitions with Induction
by: Guermond, Nathan, et al.
Published: (2025)

A Graphical Interface for Category Theory Proofs in Coq
by: Chabassier, Luc
Published: (2025)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
by: Gross, Jason, et al.
Published: (2022)

Denotational Semantics for ODRL: Knowledge-Based Constraint Conflict Detection
by: Mustafa, Daham, et al.
Published: (2026)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

The Directed Van Kampen Theorem in Lean
by: Basold, Henning, et al.
Published: (2023)

Classifying the groups of order $p q$ in Lean
by: Harper, Scott, et al.
Published: (2025)

A Formally Verified Library of Mathematical Finance in Lean 4
by: Coelho, Raphael
Published: (2026)

Axis-Aligned Semantics for ODRL: Resolving Dimensional Ambiguity in Policy Constraints
by: Mustafa, Daham, et al.
Published: (2026)

Sutra: Tensor-Op RNNs as a Compilation Target for Vector Symbolic Architectures
by: Leonhart, Emma
Published: (2026)

From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes
by: Hellwig, Jonathan, et al.
Published: (2025)

Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations
by: Beg, Arshad, et al.
Published: (2026)

Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
by: Beg, Arshad, et al.
Published: (2025)

A Short Survey on Formalising Software Requirements using Large Language Models
by: Beg, Arshad, et al.
Published: (2025)

Verified VCG and Verified Compiler for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

Towards Comprehensive Sampling of SMT Solutions
by: Lyu, Shuangyu, et al.
Published: (2025)

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
by: Klaus, Natalia, et al.
Published: (2026)

A formalization of Borel determinacy in Lean
by: Manthe, Sven
Published: (2025)

Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
by: Koomullil, George
Published: (2026)

The pitfalls of verifying floating-point computations
by: Monniaux, David
Published: (2007)

Uniform Substitution for Differential Refinement Logic
by: Prebet, Enguerrand, et al.
Published: (2024)

Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis
by: Waldinger, Richard
Published: (2025)

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
by: Prebet, Enguerrand, et al.
Published: (2026)

Approximate Algorithms for Verifying Differential Privacy with Gaussian Distributions
by: Bhusal, Bishnu, et al.
Published: (2025)

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
by: Sundaram, Aarthi, et al.
Published: (2021)

Generative Fractional Diffusion Models
by: Nobis, Gabriel, et al.
Published: (2023)

Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics
by: Beg, Arshad, et al.
Published: (2026)

Working Document -- Formalising Software Requirements with Large Language Models
by: Beg, Arshad, et al.
Published: (2025)

Evaluating LLM-Generated ACSL Annotations for Formal Verification
by: Beg, Arshad, et al.
Published: (2026)

Formalising Software Requirements using Large Language Models
by: Beg, Arshad, et al.
Published: (2025)

Graph Construction and Matching for Imperative Programs using Neural and Structural Methods
by: Beg, Arshad, et al.
Published: (2026)

On The Role of Intentionality in Knowledge Representation: Analyzing Scene Context for Cognitive Agents with a Tiny Language Model
by: Burgess, Mark
Published: (2025)

Provably Correct Systems: Community, connections, and citations
by: Bowen, Jonathan P.
Published: (2015)

Formalizing Computational Paths and Fundamental Groups in Lean
by: Ramos, Arthur F., et al.
Published: (2025)

$γ(3,4)$ `Attention' in Cognitive Agents: Ontology-Free Knowledge Representations With Promise Theoretic Semantics
by: Burgess, Mark
Published: (2025)

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations
by: Knothe, David, et al.
Published: (2026)

Bottom-up computation using trees of sublists (Functional Pearl)
by: Mu, Shin-Cheng
Published: (2023)

Precise Reasoning About Container-Internal Pointers with Logical Pinning
by: Guan, Yawen, et al.
Published: (2025)