Programming Tutorials

Excellent Free Tutorials to Learn Coq

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.

Read the tutorial


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.

Read the tutorial


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).

Read the tutorial


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.

Read the tutorial


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.

Read the tutorial


6. Video tutorials for the Coq proof assistant by Andrej Bauer

These screencasts provide a good introduction to Coq.

Watch the videos


7. Software foundations in Coq by Benjamin Pierce

These videos accompany the Software Foundations books (published in 4 volumes).

Watch the videos


All tutorials in this series:

Free Programming Tutorials
ABAPAdvanced Business Application Programming
AdaALGOL-like programming language, extended from Pascal and others
AgdaDependently typed functional language based on intuitionistic type theory
AliceEducational language with an integrated development environment
ArduinoInexpensive, flexible, open source microcontroller platform
AssemblyAs close to writing machine code without writing in pure hexadecimal
AwkVersatile language designed for pattern scanning and processing
Bash‘Bourne-Again-SHell’ is both a shell and programming language
BASICFamily of general-purpose, high-level programming languages
CGeneral-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
ChapelParallel-programming language in development at Cray Inc.
ClojureDialect of the Lisp programming language
ClojureScriptCompiler for Clojure that targets JavaScript
COBOLCommon Business-Oriented Language
CoffeeScriptA very succinct programming language that transcompiles into JavaScript
CoqDependently typed language similar to Agda, Idris, F*, Lean, and others
CrystalGeneral-purpose, concurrent, multi-paradigm, object-oriented language
CSSCSS (Cascading Style Sheets) specifies a web page’s appearance
DGeneral-purpose systems programming language with a C-like syntax
DartClient-optimized programming language for fast apps
DylanMulti-paradigm language, supports functional & object-oriented programming
ECMAScriptBest known as the language embedded in web browsers
EiffelObject-oriented language
ElixirRelatively new functional language that runs on the Erlang virtual machine
ElmFunctional language that compiles to JavaScript
Emacs LispA dialect of the Lisp programming language.
ErlangGeneral-purpose, concurrent, declarative, functional language
F#General purpose, strongly typed, multi-paradigm language. Part of ML
FactorDynamic stack-based language
ForthImperative stack-based programming language
FortranThe first high-level language, using the first compiler
GDScript Godot’s built-in language for scripting and interacting with nodes
GoCompiled, statically typed programming language
GroovyPowerful, optionally typed and dynamic language
HackFor the HipHop Virtual Machine (HHVM), created as a dialect of PHP
HamlHTML Abstraction Markup Language
HaskellStandardized, general-purpose, polymorphically, statically typed language
HTMLHyperText Markup Language
IconHigh-level, general-purpose language
ImbaFull-stack language that compiles to performant JavaScript
JArray programming language based primarily on APL
JavaGeneral-purpose, concurrent, class-based, object-oriented, high-level language
JavaScriptInterpreted, prototype-based, scripting language
JuliaHigh-level, high-performance language for technical computing
KotlinStatically typed, general-purpose programming language with type inference
LabVIEWDesigned to enable domain experts to build power systems quickly
LaTeXProfessional document preparation system and document markup language
LessBackwards-compatible language extension for Cascading Style Sheets
LimboDesigned for applications running distributed systems on small computers
LispUnique features - excellent to study programming constructs
LogoDialect of Lisp that features interactivity, modularity, extensibility
LuaDesigned as an embeddable scripting language
MarkdownPlain text formatting syntax designed to be easy-to-read and easy-to-write
MoonScriptDynamic scripting programmer friendly language that compiles into Lua
NimStatically typed compiled systems language with syntax resembling Python
Objective-CGeneral purpose language which is a superset of C
OCamlGeneral-purpose, powerful, high-level language
OctaveHigh-level language, primarily intended for numerical computations
OpenCLOpen Computing Language
PascalImperative and procedural language designed in the late 1960s
PerlHigh-level, general-purpose, interpreted, scripting, dynamic language
PikeInterpreted, general-purpose, high-level, cross-platform, dynamic language
PHPPHP has been at the helm of the web for many years
PonyPony is an actor-model, capabilities-secure, high-performance language
PostScriptPage description language in electronic and desktop publishing
PrologGeneral purpose, declarative, logic programming language
PureScriptSmall strongly, statically typed language with expressive types
PythonGeneral-purpose, structured, powerful language
QMLHierarchical declarative language for user interface layout with a syntax to JSON
RDe facto standard among statisticians and data analysts
RacketPlatform for programming language design and implementation
RakuMember of the Perl family of programming languages
RubyGeneral purpose, scripting, structured, flexible, fully object-oriented language
RustIdeal for systems, embedded, and other performance critical code
ScalaModern, object-functional, multi-paradigm, Java-based language
SchemeGeneral-purpose, functional, language descended from Lisp and Algol
ScratchVisual programming language designed for 8-16 year-old children
SolidityObject-oriented, high-level language for implementing smart contracts
SQLAccess and manipulate data held in a relational database management system
Standard MLOne of the two main dialects of the ML language
SwiftPowerful and intuitive general-purpose programming language
TclDynamic language based on concepts of Lisp, C, and Unix shells
TypeScriptStrict syntactical superset of JavaScript, adding optional static typing
VStatically typed compiled language to build maintainable software
ValaObject-oriented language with a self-hosting compiler that generates C code
VHDLVery High Speed Integrated Circuit Hardware Description Language
VimLPowerful scripting language of the Vim editor
XMLSet of rules for defining semantic tags that describe the structure and meaning
Share this article

Share your Thoughts

This site uses Akismet to reduce spam. Learn how your comment data is processed.