Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.
Users generate proofs by entering a series of tactics that constitute steps in the proof. There are many built-in tactics, some of which are elementary, while others implement complex decision procedures (such as lia, a decision procedure for linear integer arithmetic). Ltac and its planned replacement, Ltac2, provide languages to define new tactics by combining existing tactics with looping and conditional constructs. These permit automation of large parts of proofs and sometimes entire proofs. Furthermore, users can add novel tactics or functionality by creating Coq plugins using OCaml.
The Coq kernel, a small part of Coq, does the final verification that the tactic-generated proof is valid. Usually the tactic-generated proof is indeed correct, but delegating proof verification to the kernel means that even if a tactic is buggy, it won’t be able to introduce an incorrect proof into the system.
Finally, Coq also supports extraction of verified programs to programming languages such as OCaml and Haskell. This provides a way of executing Coq code efficiently and can be used to create verified software libraries.
Website: coq.inria.fr
Support: Documentation, GitHub Code Repository
Developer: INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2, Ascola, Galinette projects (starting 1985),- Laboratoire de l’Informatique du Parallelisme (LIP)
associated to CNRS and ENS Lyon (Sep. 1989 to Aug. 1997), Laboratoire de Recherche en Informatique (LRI) associated to CNRS and university Paris Sud (since Sep. 1997), Laboratoire d’Informatique de l’Ecole Polytechnique (LIX) associated to CNRS and Ecole Polytechnique (since Jan. 2003). Laboratoire PPS associated to CNRS and University Paris Diderot
License: GNU Lesser General Public License v2.1
Coq is written in OCaml and Coq. Learn OCaml with our recommended free books and free tutorials.
| Popular series | |
|---|---|
 | The largest compilation of the best free and open source software in the universe. Each article is supplied with a legendary ratings chart helping you to make informed decisions. |
 | Hundreds of in-depth reviews offering our unbiased and expert opinion on software. We offer helpful and impartial information. |
 | The Big List of Active Linux Distros is a large compilation of actively developed Linux distributions. |
 | Replace proprietary software with open source alternatives: Google, Microsoft, Apple, Adobe, IBM, Autodesk, Oracle, Atlassian, Corel, Cisco, Intuit, and SAS. |
 | Awesome Free Linux Games Tools showcases a series of tools that making gaming on Linux a more pleasurable experience. This is a new series. |
 | Machine Learning explores practical applications of machine learning and deep learning from a Linux perspective. We've written reviews of more than 40 self-hosted apps. All are free and open source. |
 | New to Linux? Read our Linux for Starters series. We start right at the basics and teach you everything you need to know to get started with Linux. |
 | Alternatives to popular CLI tools showcases essential tools that are modern replacements for core Linux utilities. |
 | Essential Linux system tools focuses on small, indispensable utilities, useful for system administrators as well as regular users. |
 | Linux utilities to maximise your productivity. Small, indispensable tools, useful for anyone running a Linux machine. |
 | Surveys popular streaming services from a Linux perspective: Amazon Music Unlimited, Myuzi, Spotify, Deezer, Tidal. |
 | Saving Money with Linux looks at how you can reduce your energy bills running Linux. |
 | Home computers became commonplace in the 1980s. Emulate home computers including the Commodore 64, Amiga, Atari ST, ZX81, Amstrad CPC, and ZX Spectrum. |
 | Now and Then examines how promising open source software fared over the years. It can be a bumpy ride. |
 | Linux at Home looks at a range of home activities where Linux can play its part, making the most of our time at home, keeping active and engaged. |
 | Linux Candy reveals the lighter side of Linux. Have some fun and escape from the daily drudgery. |
 | Getting Started with Docker helps you master Docker, a set of platform as a service products that delivers software in packages called containers. |
 | Best Free Android Apps. We showcase free Android apps that are definitely worth downloading. There's a strict eligibility criteria for inclusion in this series. |
 | These best free books accelerate your learning of every programming language. Learn a new language today! |
 | These free tutorials offer the perfect tonic to our free programming books series. |
 | Linux Around The World showcases usergroups that are relevant to Linux enthusiasts. Great ways to meet up with fellow enthusiasts. |
 | Stars and Stripes is an occasional series looking at the impact of Linux in the USA. |