A Brief Overview of Agda - A Functional Language with Dependent Types

Abstract. We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-L¨of’s intuitionistic type theory but extends it with numerous programming language features. It supports a wide range of inductive data types, including inductive families and inductive-recursive types, with associated flexible pattern-matching. Unlike other proof assistants, Agda is not tactic-based. Instead it has an Emacs-based interface which allows programming by gradual refinement of incomplete type-correct terms.

• Type: Conference
• Year: 2009
• Where: TPHOL
• Authors: Ana Bove, Peter Dybjer, Ulf Norell
• Keywords: Artificial Intelligence, Inductive Data Types, Intuitionistic Type Theory, Programming Language, TPHOL 2009