Sciweavers

TPHOL
2009
IEEE

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

13 years 10 months ago
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.
Ana Bove, Peter Dybjer, Ulf Norell
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where TPHOL
Authors Ana Bove, Peter Dybjer, Ulf Norell
Comments (0)