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öf'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. © 2009 Springer.
Cite
CITATION STYLE
Bove, A., Dybjer, P., & Norell, U. (2009). A brief overview of Agda - A functional language with dependent types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5674 LNCS, pp. 73–78). https://doi.org/10.1007/978-3-642-03359-9_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
