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 | |
|---|---|
| Ada | ALGOL-like programming language, extended from Pascal and other languages |
| Agda | Dependently typed functional language based on intuitionistic Type Theory |
| 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 language |
| Bash | Shell and command language; popular both as a shell and a scripting language |
| BASIC | Beginner’s All-purpose Symbolic Instruction Code |
| 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 |
| Clojure | Dialect of the Lisp programming language |
| ClojureScript | Compiler for Clojure that targets JavaScript |
| COBOL | Common Business-Oriented Language |
| CoffeeScript | Transcompiles into JavaScript inspired by Ruby, Python and Haskell |
| Coq | Dependently typed language similar to Agda, Idris, F* 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 language for fast apps on multiple platforms |
| Dylan | Multi-paradigm language supporting functional and object-oriented coding |
| ECMAScript | Best known as the language embedded in web browsers |
| Eiffel | Object-oriented language designed by Bertrand Meyer |
| Elixir | Relatively new functional language running on the Erlang virtual machine |
| Erlang | General-purpose, concurrent, declarative, functional language |
| F# | Uses functional, imperative, and object-oriented programming methods |
| Factor | Dynamic stack-based programming language |
| Forth | Imperative stack-based programming language |
| Fortran | The first high-level language, using the first compiler |
| Go | Compiled, statically typed programming language |
| Groovy | Powerful, optionally typed and dynamic language |
| Haskell | Standardized, general-purpose, polymorphically, statically typed language |
| HTML | HyperText Markup Language |
| Icon | Wide variety of features for processing and presenting symbolic data |
| 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 | More modern version of Java |
| LabVIEW | Designed to enable domain experts to build power systems quickly |
| LaTeX | Professional document preparation system and document markup language |
| 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 |
| Objective-C | Object-oriented language that adds Smalltalk-style messaging to C |
| OCaml | The main implementation of the Caml language |
| Pascal | Imperative and procedural language designed in the late 1960s |
| Perl | High-level, general-purpose, interpreted, scripting, dynamic language |
| PHP | PHP has been at the helm of the web for many years |
| PostScript | Interpreted, stack-based and Turing complete language |
| Prolog | A general purpose, declarative, logic programming language |
| PureScript | Small strongly, statically typed language compiling to JavaScript |
| Python | General-purpose, structured, powerful language |
| QML | Hierarchical declarative language for user interface layout - JSON-like syntax |
| R | De facto standard among statisticians and data analysts |
| Racket | General-purpose, object-oriented, multi-paradigm, functional language |
| Raku | Member of the Perl family of programming languages |
| 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 | A general-purpose, functional language descended from Lisp and Algol |
| Scratch | Visual programming language designed for 8-16 year-old children |
| SQL | Access and manipulate data held in a relational database management system |
| Standard ML | General-purpose functional language characterized as "Lisp with types" |
| Swift | Powerful and intuitive general-purpose programming language |
| Tcl | Dynamic language based on concepts of Lisp, C, and Unix shells |
| TeX | Markup and programming language - create professional quality typeset text |
| TypeScript | Strict syntactical superset of JavaScript adding optional static typing |
| Vala | Object-oriented language, syntactically similar to C# |
| VHDL | Hardware description language used in electronic design automation |
| VimL | Powerful scripting language of the Vim editor |
| XML | Rules for defining semantic tags describing structure ad meaning |