This paper reports on a six-year collaborative effort that culminated in a complete
formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant …

Abstract Development of formal proofs of correctness of programs can increase actual and
perceived reliability and facilitate better understanding of program specifications and their …

Hammers provide most powerful general purpose automation for proof assistants based on
HOL and set theory today. Despite the gaining popularity of the more advanced versions of …

This paper describes SMTCoq, a plug-in for the integration of external solvers into the Coq
proof assistant. Based on a checker for generic first-order proof certificates fully implemented …

By interactive theorem proving, we mean some arrangement where the machine and a
human user work together interactively to produce a formal proof. There is a wide spectrum …

Integrating property-based testing with a proof assistant creates an interesting opportunity:
reusable or tricky testing code can be formally verified using the proof assistant itself. In this …

Interactive theorem provers have developed dramatically over the past four decades, from
primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its …

The C programming language was created by Thompson and Ritchie around 1970 as the
implementation language of the Unix operating system [Rit93]. The development of Unix …

We design and implement Zooid, a domain specific language for certified multiparty
communication, embedded in Coq and implemented atop our mechanisation framework of …

This paper gives an introduction to the Calculus of Inductive Constructions, the formalism
behind the Coq proof assistant. We present the language and the typing rules, starting with …