30 years of research and development around Coq

DOI10.1145/2535838.2537848zbMath1284.68517OpenAlexW2055815710MaRDI QIDQ5408420

Gérard Huet, Hugo Herbelin

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2535838.2537848

zbMATH Keywords

proof assistantformalization of mathematicsinteractive theorem provingCoqcalculus of inductive constructionscertified programming

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) History of computer science (68-03)

Related Items

JEFL: joint embedding of formal proof libraries, Programming and Proving with Classical Types, Aligning concepts across proof assistant libraries, Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points, Coq