A Brief Overview of Agda

A Brief Overview of Agda {A Functional Language with Dependent TypesAna Bove, Peter Dybjer, and Ulf Norelle-mail:fbove,peterd,ulfng@chalmers.seChalmers University of Technology, Gothenburg, SwedenAbstract. We give an overview of Agda, the latest in a series of depen-dently typed programming languages developed in Gothenburg. Agdais based on Martin-L of’s intuitionistic type theory but extends it withnumerous language features. It supports a wide range ofinductive data types, including inductive families and inductive-recursivetypes, with associated exible pattern-matching. Unlike other proof as-sistants, Agda is not tactic-based. Instead it has an Emacs-based in-terface which allows programming by gradual re nement of incompletetype-correct terms.1 IntroductionA dependently typed programming language and proof assistant. Agda is a func-tional programming language with dependent types. It is an extension of Martin-L of’s intuitionistic type theory [12, 13] with numerous features which are usefulfor practical programming. Agda is also a proof assistant. By the Curry-Howardidenti cation, we can represent logical propositions by types. A proposition isproved by writing a program of the corresponding type. However, Agda is pri-marily being developed as a programming language and not as a proof assistant.Agda is the latest in a series of implementations of intensional type theorywhich have been developed in Gothenburg (beginning with the ...