Cover Image

A Natural Formalized Proof Language

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Xie, Lihan, Hui, Zhicheng, Cao, Qinxiang
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
by: Yang, Chengxi, et al.
Published: (2025)

Stellis: A Strategy Language for Purifying Separation Logic Entailments
by: Wang, Zhiyi, et al.
Published: (2025)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
by: Wu, Shushu, et al.
Published: (2025)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

Denotation-based Compositional Compiler Verification
by: Cheng, Zhang, et al.
Published: (2024)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
by: Liu, Chang, et al.
Published: (2023)

CktFormalizer: Autoformalization of Natural Language into Circuit Representations
by: Xiong, Jing, et al.
Published: (2026)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
by: Ravi, Nikil, et al.
Published: (2026)

Linguine: A Natural-Language Programming Language with Formal Semantics and a Clean Compiler Pipeline
by: Hu, Lifan
Published: (2025)

QCP: A Practical Separation Logic-based C Program Verification Tool
by: Wu, Xiwei, et al.
Published: (2025)

From a Natural to a Formal Language with DSL Assistant
by: Mosthaf, My M., et al.
Published: (2024)

Automated Formalization of Probabilistic Requirements from Structured Natural Language
by: Mavridou, Anastasia, et al.
Published: (2025)

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
by: Councilman, Aaron, et al.
Published: (2025)

Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
by: Endres, Madeline, et al.
Published: (2023)

A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
by: Xu, Qiyuan, et al.
Published: (2025)

FLAT: Formal Languages as Types
by: Zhu, Fengmin, et al.
Published: (2025)

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

Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
by: Zhao, Jianhong, et al.
Published: (2025)

Minuska: Towards a Formally Verified Programming Language Framework
by: Tušil, Jan, et al.
Published: (2024)

C*: Unifying Programming and Verification in C
by: Cao, Yiyuan, et al.
Published: (2025)

Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure
by: Hattori, Seiji, et al.
Published: (2025)

The Formal Semantics and Implementation of a Domain-Specific Language for Mixed-Initiative Dialogs
by: Rowland, Zachary S., et al.
Published: (2025)

Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
by: Xia, Shihao, et al.
Published: (2026)

Agentic Proof Automation: A Case Study
by: Xu, Yichen, et al.
Published: (2026)

Learning to Guarantee Type Correctness in Code Generation through Type-Guided Program Synthesis
by: Huang, Zhechong, et al.
Published: (2025)

A Brief Survey of Formal Models of Concurrency
by: Averill, Charles
Published: (2024)

ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
by: Gu, Alex, et al.
Published: (2025)

From Algebraic Word Problem to Program: A Formalized Approach
by: Wiemerslage, Adam, et al.
Published: (2020)

Automating Equational Proofs in Dirac Notation
by: Xu, Yingte, et al.
Published: (2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
by: Parthasarathy, Gaurav, et al.
Published: (2024)

VyZX: Formal Verification of a Graphical Quantum Language
by: Lehmann, Adrian, et al.
Published: (2023)

Practical Formal Verification for MLIR Programs
by: Tucker, Emily, et al.
Published: (2026)

$φ$-Calculus: Object-Oriented Formalism
by: Bugayenko, Yegor, et al.
Published: (2021)

Proof Repair across Quotient Type Equivalences
by: Viola, Cosmo, et al.
Published: (2023)

Adaptive Shielding via Parametric Safety Proofs
by: Feng, Yao, et al.
Published: (2025)

Asynchronous Global Protocols, Precisely: Full Proofs
by: Pischke, Kai, et al.
Published: (2025)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
by: Liu, Qi, et al.
Published: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

Synthesizing Formal Semantics from Executable Interpreters
by: Liu, Jiangyi, et al.
Published: (2024)