Last Updated on June 12, 2023
Coq is a dependently typed language. This means that the types of the language may depend on the values of variables. In this respect, it is similar to other related languages such as Agda, Idris, F*, Lean, and others. Via the Curry-Howard correspondence, programs, properties and proofs are formalized in the same language.
Coq is developed in OCaml and shares some syntactic and conceptual similarity with it. Coq is a language containing many fascinating but difficult topics.
Here’s our recommended tutorials to learn Coq.
1. Coq in a Hurry by Yves Bertot
These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system.
2. Learn Coq in Y Minutes by Philip Zucker
The Coq system is a proof assistant. It is designed to build and verify mathematical proofs. The Coq system contains the functional programming language Gallina and is capable of proving properties about programs written in this language.
This tutorial focuses on the programming aspects of Coq, rather than the proving. It may be helpful, but not necessary to learn some OCaml first, especially if you are unfamiliar with functional programming. This tutorial is based upon its OCaml equivalent.
3. An Introduction to the Coq Proof Assistant by Arthur Azevedo de Amorim and Robert Rand
This tutorial focuses on functional programming and mathematical proofs using the Coq proof assistant.
By the end of the tutorial, participants should be able to: Write simple functional programs in Coq, write precise program specifications, and connect 1 and 2 via formal proofs.
This tutorial is aimed at programmers with some knowledge of functional programming who are interested in writing highly reliable programs in Coq or a related language (such as Haskell, Agda or Isabelle).
4. A Tutorial on [Co-]Inductive Types in Coq by Eduardo Giménez and Pierre Castéran
This tutorial is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are defined in Coq, and the kind of proof techniques that can be used to reason about them (case analysis, induction, inversion of predicates, co-induction, etc). Each technique is illustrated
through an executable and self-contained Coq script.
5. A Gentle Introduction to Type Classes and Relations in Coq by Pierre Castéran
This tutorial provides a concise introduction to two important features of the Coq proof assistant: type classes and user defined relations.
6. Video tutorials for the Coq proof assistant by Andrej Bauer
These screencasts provide a good introduction to Coq.
7. Software foundations in Coq by Benjamin Pierce
These videos accompany the Software Foundations books (published in 4 volumes).
All tutorials in this series:
| Free Programming Tutorials | |
|---|---|
| ABAP | Advanced Business Application Programming |
| Ada | ALGOL-like programming language, extended from Pascal and others |
| Agda | Dependently typed functional language based on intuitionistic type theory |
| Alice | Educational language with an integrated development environment |
| Arduino | Inexpensive, flexible, open source microcontroller platform |
| Assembly | As close to writing machine code without writing in pure hexadecimal |
| Awk | Versatile language designed for pattern scanning and processing |
| Bash | ‘Bourne-Again-SHell’ is both a shell and programming language |
| BASIC | Family of general-purpose, high-level programming languages |
| C | General-purpose, procedural, portable, high-level language |
| C++ | General-purpose, portable, free-form, multi-paradigm language |
| C# | Combines the power and flexibility of C++ with the simplicity of Visual Basic |
| Chapel | Parallel-programming language in development at Cray Inc. |
| Clojure | Dialect of the Lisp programming language |
| ClojureScript | Compiler for Clojure that targets JavaScript |
| COBOL | Common Business-Oriented Language |
| CoffeeScript | A very succinct programming language that transcompiles into JavaScript |
| Coq | Dependently typed language similar to Agda, Idris, F*, Lean, and others |
| Crystal | General-purpose, concurrent, multi-paradigm, object-oriented language |
| CSS | CSS (Cascading Style Sheets) specifies a web page’s appearance |
| D | General-purpose systems programming language with a C-like syntax |
| Dart | Client-optimized programming language for fast apps |
| Dylan | Multi-paradigm language, supports functional & object-oriented programming |
| ECMAScript | Best known as the language embedded in web browsers |
| Eiffel | Object-oriented language |
| Elixir | Relatively new functional language that runs on the Erlang virtual machine |
| Elm | Functional language that compiles to JavaScript |
| Emacs Lisp | A dialect of the Lisp programming language. |
| Erlang | General-purpose, concurrent, declarative, functional language |
| F# | General purpose, strongly typed, multi-paradigm language. Part of ML |
| Factor | Dynamic stack-based language |
| Forth | Imperative stack-based programming language |
| Fortran | The first high-level language, using the first compiler |
| GDScript | Godot’s built-in language for scripting and interacting with nodes |
| Go | Compiled, statically typed programming language |
| Groovy | Powerful, optionally typed and dynamic language |
| Hack | For the HipHop Virtual Machine (HHVM), created as a dialect of PHP |
| Haml | HTML Abstraction Markup Language |
| Haskell | Standardized, general-purpose, polymorphically, statically typed language |
| HTML | HyperText Markup Language |
| Icon | High-level, general-purpose language |
| Imba | Full-stack language that compiles to performant JavaScript |
| J | Array programming language based primarily on APL |
| Java | General-purpose, concurrent, class-based, object-oriented, high-level language |
| JavaScript | Interpreted, prototype-based, scripting language |
| Julia | High-level, high-performance language for technical computing |
| Kotlin | Statically typed, general-purpose programming language with type inference |
| LabVIEW | Designed to enable domain experts to build power systems quickly |
| LaTeX | Professional document preparation system and document markup language |
| Less | Backwards-compatible language extension for Cascading Style Sheets |
| Limbo | Designed for applications running distributed systems on small computers |
| Lisp | Unique features - excellent to study programming constructs |
| Logo | Dialect of Lisp that features interactivity, modularity, extensibility |
| Lua | Designed as an embeddable scripting language |
| Markdown | Plain text formatting syntax designed to be easy-to-read and easy-to-write |
| MoonScript | Dynamic scripting programmer friendly language that compiles into Lua |
| Nim | Statically typed compiled systems language with syntax resembling Python |
| Objective-C | General purpose language which is a superset of C |
| OCaml | General-purpose, powerful, high-level language |
| Octave | High-level language, primarily intended for numerical computations |
| OpenCL | Open Computing Language |
| Pascal | Imperative and procedural language designed in the late 1960s |
| Perl | High-level, general-purpose, interpreted, scripting, dynamic language |
| Pike | Interpreted, general-purpose, high-level, cross-platform, dynamic language |
| PHP | PHP has been at the helm of the web for many years |
| Pony | Pony is an actor-model, capabilities-secure, high-performance language |
| PostScript | Page description language in electronic and desktop publishing |
| Prolog | General purpose, declarative, logic programming language |
| PureScript | Small strongly, statically typed language with expressive types |
| Python | General-purpose, structured, powerful language |
| QML | Hierarchical declarative language for user interface layout with a syntax to JSON |
| R | De facto standard among statisticians and data analysts |
| Racket | Platform for programming language design and implementation |
| Raku | Member of the Perl family of programming languages |
| Roff | Extensible text formatting language and a set of programs for printing |
| Ruby | General purpose, scripting, structured, flexible, fully object-oriented language |
| Rust | Ideal for systems, embedded, and other performance critical code |
| Scala | Modern, object-functional, multi-paradigm, Java-based language |
| Scheme | General-purpose, functional, language descended from Lisp and Algol |
| Scratch | Visual programming language designed for 8-16 year-old children |
| Solidity | Object-oriented, high-level language for implementing smart contracts |
| SQL | Access and manipulate data held in a relational database management system |
| Standard ML | One of the two main dialects of the ML language |
| Swift | Powerful and intuitive general-purpose programming language |
| Tcl | Dynamic language based on concepts of Lisp, C, and Unix shells |
| TypeScript | Strict syntactical superset of JavaScript, adding optional static typing |
| V | Statically typed compiled language to build maintainable software |
| Vala | Object-oriented language with a self-hosting compiler that generates C code |
| VHDL | Very High Speed Integrated Circuit Hardware Description Language |
| VimL | Powerful scripting language of the Vim editor |
| XML | Set of rules for defining semantic tags that describe the structure and meaning |
| Zig | General-purpose programming language and toolchain |