We present a way to enjoy the power of SAT and SMT provers in Coq without compromising
soundness. This requires these provers to return not only a yes/no answer, but also a proof …

The introduction of first-class type classes in the Coq system calls for a re-examination of the
basic interfaces used for mathematical formalisation in type theory. We present a new set of …

The MetaCoq project aims to provide a certified meta-programming environment in Coq. It
builds on Template-Coq, a plugin for Coq originally implemented by Malecha (Extensible …

Abstract Template-Coq (https://template-coq. github. io/template-coq) is a plugin for Coq,
originally implemented by Malecha 18, which provides a reifier for Coq terms and global …

This paper is a tutorial on using the Coq proof-assistant for reasoning on software
correctness. It illustrates features of Coq like inductive definitions and proof automation on a …

Type inference is essential for statically-typed languages such as OCaml and Haskell. It can
be decomposed into two (possibly interleaved) phases: a generator converts programs to …

Floating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to
approximate real numbers. Due to its limited range and precision, its use can become quite …

Effective support for custom proof automation is essential for large-scale interactive proof
development. However, existing languages for automation via tactics either (a) provide no …

This paper presents versat, a formally verified SAT solver incorporating the essential
features of modern SAT solvers, including clause learning, watched literals, optimized …

Floating point operations are fast, but require continuous effort on the part of the user in
order to ensure that the results are correct. This burden can be shifted away from the user by …