A proof system for MSVL programs in Coq

DOI10.1007/978-3-319-57708-1_8MaRDI QIDQ4989018zbMATH OpenOpenAlexFDO

Authors Lin Qian, Zhenhua Duan, Nan Zhang, Cong Tian

Publication date 20 May 2021

Published in Structured Object-Oriented Formal Language and Method (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-57708-1_8

zbMATH Keywords

Coqinteractive theorem proverMSVLsemi-automatic proof

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Synthesis of ML programs in the system Coq
• scientific article; zbMATH DE number 6296049
• Axiomatic semantics of projection temporal logic programs
• Theorem-proving support in programming language semantics
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.

Cited in

(8)

• Proof reflection in Coq
• Translating Xd-C programs to MSVL programs
• scientific article; zbMATH DE number 1670739 (Why is no real title available?)
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Proving tight bounds on univariate expressions with elementary functions in Coq
• scientific article; zbMATH DE number 1301729 (Why is no real title available?)
• A mechanized proof system of the third generation calculus in Coq
• Proof by computation in the Coq system

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A proof system for MSVL programs in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4989018)