Free Programming Books

4 Excellent Free Books to Learn Agda and Type Theory

Agda is a dependently typed functional programming language based on intuitionistic Type Theory. Type theory is concerned both with programming and logic.

It’s an extension of Martin-Löf’s type theory, and is the latest in the tradition of languages developed in the programming logic group at Chalmers. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrized modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. Other languages in this tradition are Alf, Alfa, Agda 1, Cayenne. Some other loosely related languages are Coq, Epigram, and Idris.

Agda is also a proof assistant based on the propositions-as-types paradigm, but has no separate tactics language, and proofs are written in a functional programming style.

Agda is open-source and enjoys contributions from many authors. The center of the Agda development is the Programming Logic group at Chalmers and Gothenburg University.

Here’s our recommended free books to learn about Agda and Type Theory.


1. Programming Languages Foundations in Agda by Philip Wadler with contributions from Wen Kokke, Jeremy Siek

 Programming Language Foundations in AgdaProgramming Languages Foundations in Agda is an introduction to programming language theory using the proof assistant Agda.

This book offers good coverage of logical foundations and programming language foundations. The book is broken into two parts. The first part, Logical Foundations, develops the needed formalisms. The second part, Programming Language Foundations, introduces basic methods of operational semantics.

Programming Languages Foundations in Agda is licensed under a Creative Commons Attribution 4.0 International License.

Read the book


2. Agda User Manual by The Agda Team

Agda User ManualThis is the manual for the Agda programming language, its type checking, compilation and editing system and related resources/tools.

A detailed description of the Agda language is given in the Language Reference chapter looking at built-ins, coinduction, copatterns, data types, function types, lambda abstraction, module system, postulates, prop, and much more.

Guidance on how the Agda editing and compilation system can be used can be found in the Tools chapter.

Read the manual


3. Programming in Martin-Löf’s Type Theory by Bengt Nordström, Kent Petersson, Jan M. Smith

Programming in Martin-Löf’s Type TheoryProgramming in Martin-Löf’s Type Theory describes different type theories (theories of types, polymorphic and monomorphic sets, and subsets) from a computing science perspective.

It’s intended for researchers and graduate students with an interest in the foundations of computing science, and it’s mathematically self-contained.

This book was published by Oxford University Press in 1990. It is now out of print.

Read the book


4. Towards a practical programming language based on dependent type theory by Ulf Norell

Towards a practical programming language based on dependent type theoryThis thesis is concerned with bridging the gap between the theoretical presentations of type theory and the requirements on a practical programming language.

The author presents a type checking algorithm for a theory with metavariables and prove its soundness independent of whether the metavariables are solved or not.

The thesis ends with the implementation of a programming language, Agda, based on type theory. As an illustrating example, the author shows how to program a simple certified prover for equations in a commutative monoid, which can be used internally in Agda.

Read the thesis


All books in this series:

Free Programming Books
JavaGeneral-purpose, concurrent, class-based, object-oriented, high-level language
CGeneral-purpose, procedural, portable, high-level language
PythonGeneral-purpose, structured, powerful language
C++General-purpose, portable, free-form, multi-paradigm language
C#Combines the power and flexibility of C++ with the simplicity of Visual Basic
JavaScriptInterpreted, prototype-based, scripting language
PHPPHP has been at the helm of the web for many years
HTMLHyperText Markup Language
SQLAccess and manipulate data held in a relational database management system
RubyGeneral purpose, scripting, structured, flexible, fully object-oriented language
AssemblyAs close to writing machine code without writing in pure hexadecimal
SwiftPowerful and intuitive general-purpose programming language
GroovyPowerful, optionally typed and dynamic language
GoCompiled, statically typed programming language
PascalImperative and procedural language designed in the late 1960s
PerlHigh-level, general-purpose, interpreted, scripting, dynamic language
RDe facto standard among statisticians and data analysts
COBOLCommon Business-Oriented Language
ScalaModern, object-functional, multi-paradigm, Java-based language
FortranThe first high-level language, using the first compiler
ScratchVisual programming language designed for 8-16 year-old children
LuaDesigned as an embeddable scripting language
LogoDialect of Lisp that features interactivity, modularity, extensibility
RustIdeal for systems, embedded, and other performance critical code
LispUnique features - excellent to study programming constructs
AdaALGOL-like programming language, extended from Pascal and other languages
HaskellStandardized, general-purpose, polymorphically, statically typed language
SchemeA general-purpose, functional language descended from Lisp and Algol
PrologA general purpose, declarative, logic programming language
ForthImperative stack-based programming language
ClojureDialect of the Lisp programming language
JuliaHigh-level, high-performance language for technical computing
AwkVersatile language designed for pattern scanning and processing language
CoffeeScriptTranscompiles into JavaScript inspired by Ruby, Python and Haskell
BASICBeginner’s All-purpose Symbolic Instruction Code
ErlangGeneral-purpose, concurrent, declarative, functional language
VimLPowerful scripting language of the Vim editor
OCamlThe main implementation of the Caml language
ECMAScriptBest known as the language embedded in web browsers
BashShell and command language; popular both as a shell and a scripting language
LaTeXProfessional document preparation system and document markup language
TeXMarkup and programming language - create professional quality typeset text
ArduinoInexpensive, flexible, open source microcontroller platform
TypeScriptStrict syntactical superset of JavaScript adding optional static typing
ElixirRelatively new functional language running on the Erlang virtual machine
F#Uses functional, imperative, and object-oriented programming methods
TclDynamic language based on concepts of Lisp, C, and Unix shells
FactorDynamic stack-based programming language
EiffelObject-oriented language designed by Bertrand Meyer
AgdaDependently typed functional language based on intuitionistic Type Theory
IconWide variety of features for processing and presenting symbolic data
XMLRules for defining semantic tags describing structure ad meaning
ValaObject-oriented language, syntactically similar to C#
Standard MLGeneral-purpose functional language characterized as "Lisp with types"
DGeneral-purpose systems programming language with a C-like syntax
Share this article

Share your Thoughts

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