Tools on Rewriting
-
Agda is a dependently typed functional programming language. 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 parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory.
* (2018-10-29) Agda 2.5.4.2 is now available. ... Page last modified on October 29, 2018, at 05:08 PM...