Programming Books

4 Excellent Free Books to Learn Agda and Type Theory

Last Updated on January 21, 2024

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
AdaALGOL-like programming language, extended from Pascal and other languages
AgdaDependently typed functional language based on intuitionistic Type Theory
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 language
BashShell and command language; popular both as a shell and a scripting language
BASICBeginner’s All-purpose Symbolic Instruction Code
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
ClojureDialect of the Lisp programming language
ClojureScriptCompiler for Clojure that targets JavaScript
COBOLCommon Business-Oriented Language
CoffeeScriptTranscompiles into JavaScript inspired by Ruby, Python and Haskell
CoqDependently typed language similar to Agda, Idris, F* 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 language for fast apps on multiple platforms
DylanMulti-paradigm language supporting functional and object-oriented coding
ECMAScriptBest known as the language embedded in web browsers
EiffelObject-oriented language designed by Bertrand Meyer
ElixirRelatively new functional language running on the Erlang virtual machine
ErlangGeneral-purpose, concurrent, declarative, functional language
F#Uses functional, imperative, and object-oriented programming methods
FactorDynamic stack-based programming language
ForthImperative stack-based programming language
FortranThe first high-level language, using the first compiler
GoCompiled, statically typed programming language
GroovyPowerful, optionally typed and dynamic language
HaskellStandardized, general-purpose, polymorphically, statically typed language
HTMLHyperText Markup Language
IconWide variety of features for processing and presenting symbolic data
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
KotlinMore modern version of Java
LabVIEWDesigned to enable domain experts to build power systems quickly
LaTeXProfessional document preparation system and document markup language
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
Objective-CObject-oriented language that adds Smalltalk-style messaging to C
OCamlThe main implementation of the Caml language
PascalImperative and procedural language designed in the late 1960s
PerlHigh-level, general-purpose, interpreted, scripting, dynamic language
PHPPHP has been at the helm of the web for many years
PostScriptInterpreted, stack-based and Turing complete language
PrologA general purpose, declarative, logic programming language
PureScriptSmall strongly, statically typed language compiling to JavaScript
PythonGeneral-purpose, structured, powerful language
QMLHierarchical declarative language for user interface layout - JSON-like syntax
RDe facto standard among statisticians and data analysts
RacketGeneral-purpose, object-oriented, multi-paradigm, functional language
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
SchemeA general-purpose, functional language descended from Lisp and Algol
ScratchVisual programming language designed for 8-16 year-old children
SQLAccess and manipulate data held in a relational database management system
Standard MLGeneral-purpose functional language characterized as "Lisp with types"
SwiftPowerful and intuitive general-purpose programming language
TclDynamic language based on concepts of Lisp, C, and Unix shells
TeXMarkup and programming language - create professional quality typeset text
TypeScriptStrict syntactical superset of JavaScript adding optional static typing
ValaObject-oriented language, syntactically similar to C#
VHDLHardware description language used in electronic design automation
VimLPowerful scripting language of the Vim editor
XMLRules for defining semantic tags describing structure ad meaning
Notify of

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

Inline Feedbacks
View all comments