Developing certified programs in the system Coq the program tactic

DOI10.1007/3-540-58085-9_81MaRDI QIDQ6083698zbMATH OpenFDO

Authors Christine Parent

Publication date 8 December 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-58085-9_81

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Synthesis of ML programs in the system Coq
• Verifying programs in the calculus of inductive constructions
• scientific article; zbMATH DE number 2003158
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Proofs and programs: A naïve approach to program extraction

Cites work

• A Complete Proof Synthesis Method for the Cube of Type Systems
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 863013 (Why is no real title available?)
• Introduction to generalized type systems
• Synthesis of ML programs in the system Coq

Cited in

(1)

• The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq

This page was built for publication: Developing certified programs in the system Coq the program tactic

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