Developing certified programs in the system Coq the program tactic

DOI10.1007/3-540-58085-9_81zbMath1527.68134MaRDI QIDQ6083698

Christine Parent

Publication date: 8 December 2023

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

Mathematics Subject Classification ID

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

Cites Work

• Synthesis of ML programs in the system Coq
• A Complete Proof Synthesis Method for the Cube of Type Systems
• Introduction to generalized type systems
• Unnamed Item
• Unnamed Item
• Unnamed Item

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