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 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.
2. Agda User Manual by The Agda Team
This 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.
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 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.
4. Towards a practical programming language based on dependent type theory by Ulf Norell
This 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.
All books in this series:
| Free Programming Books | |
|---|---|
| Java | General-purpose, concurrent, class-based, object-oriented, high-level language |
| C | General-purpose, procedural, portable, high-level language |
| Python | General-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 |
| JavaScript | Interpreted, prototype-based, scripting language |
| PHP | PHP has been at the helm of the web for many years |
| HTML | HyperText Markup Language |
| SQL | Access and manipulate data held in a relational database management system |
| Ruby | General purpose, scripting, structured, flexible, fully object-oriented language |
| Assembly | As close to writing machine code without writing in pure hexadecimal |
| Swift | Powerful and intuitive general-purpose programming language |
| Groovy | Powerful, optionally typed and dynamic language |
| Go | Compiled, statically typed programming language |
| Pascal | Imperative and procedural language designed in the late 1960s |
| Perl | High-level, general-purpose, interpreted, scripting, dynamic language |
| R | De facto standard among statisticians and data analysts |
| COBOL | Common Business-Oriented Language |
| Scala | Modern, object-functional, multi-paradigm, Java-based language |
| Fortran | The first high-level language, using the first compiler |
| Scratch | Visual programming language designed for 8-16 year-old children |
| Lua | Designed as an embeddable scripting language |
| Logo | Dialect of Lisp that features interactivity, modularity, extensibility |
| Rust | Ideal for systems, embedded, and other performance critical code |
| Lisp | Unique features - excellent to study programming constructs |
| Ada | ALGOL-like programming language, extended from Pascal and other languages |
| Haskell | Standardized, general-purpose, polymorphically, statically typed language |
| Scheme | A general-purpose, functional language descended from Lisp and Algol |
| Prolog | A general purpose, declarative, logic programming language |
| Forth | Imperative stack-based programming language |
| Clojure | Dialect of the Lisp programming language |
| Julia | High-level, high-performance language for technical computing |
| Awk | Versatile language designed for pattern scanning and processing language |
| CoffeeScript | Transcompiles into JavaScript inspired by Ruby, Python and Haskell |
| BASIC | Beginner’s All-purpose Symbolic Instruction Code |
| Erlang | General-purpose, concurrent, declarative, functional language |
| VimL | Powerful scripting language of the Vim editor |
| OCaml | The main implementation of the Caml language |
| ECMAScript | Best known as the language embedded in web browsers |
| Bash | Shell and command language; popular both as a shell and a scripting language |
| LaTeX | Professional document preparation system and document markup language |
| TeX | Markup and programming language - create professional quality typeset text |
| Arduino | Inexpensive, flexible, open source microcontroller platform |
| TypeScript | Strict syntactical superset of JavaScript adding optional static typing |
| Elixir | Relatively new functional language running on the Erlang virtual machine |
| F# | Uses functional, imperative, and object-oriented programming methods |
| Tcl | Dynamic language based on concepts of Lisp, C, and Unix shells |
| Factor | Dynamic stack-based programming language |
| Eiffel | Object-oriented language designed by Bertrand Meyer |
| Agda | Dependently typed functional language based on intuitionistic Type Theory |
| Icon | Wide variety of features for processing and presenting symbolic data |
| XML | Rules for defining semantic tags describing structure ad meaning |
| Vala | Object-oriented language, syntactically similar to C# |
| Standard ML | General-purpose functional language characterized as "Lisp with types" |
| D | General-purpose systems programming language with a C-like syntax |
| Dart | Client-optimized language for fast apps on multiple platforms |
| Markdown | Plain text formatting syntax designed to be easy-to-read and easy-to-write |
| Kotlin | More modern version of Java |
| Objective-C | Object-oriented language that adds Smalltalk-style messaging to C |
| PureScript | Small strongly, statically typed language compiling to JavaScript |
| ClojureScript | Compiler for Clojure that targets JavaScript |
| VHDL | Hardware description language used in electronic design automation |
| J | Array programming language based primarily on APL |
| LabVIEW | Designed to enable domain experts to build power systems quickly |