:: Library Catalog

Cover Image

Saved in:

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

Similar Items

Lean4Lean: Verifying a Typechecker for Lean, in Lean
by: Carneiro, Mario
Published: (2024)

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)

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

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

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

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

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)

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

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

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

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)

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

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)

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)

Towards Weak Stratification for Logics of Definitions
by: Guermond, Nathan
Published: (2026)

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
by: Baier, Daniel, et al.
Published: (2024)

MoXIchecker: An Extensible Model Checker for MoXI
by: Ates, Salih, et al.
Published: (2024)

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

Stratified Type Theory
by: Chan, Jonathan, et al.
Published: (2023)

Argumentation and Machine Learning
by: Rago, Antonio, et al.
Published: (2024)

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

Seamless, Correct, and Generic Programming over Serialised Data
by: Allais, Guillaume
Published: (2023)

"What Is It That You Don't Understand?" Language Games and Black Box Algorithms
by: Demichelis, Remy
Published: (2026)

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

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

ConfigSpec: Profiling-Based Configuration Selection for Distributed Edge--Cloud Speculative LLM Serving
by: Li, Xiangchen, et al.
Published: (2026)

WISP: Waste- and Interference-Suppressed Distributed Speculative LLM Serving at the Edge via Dynamic Drafting and SLO-Aware Batching
by: Li, Xiangchen, et al.
Published: (2026)