A Brief Overview of Agda – A Functional Language with Dependent Types Export

@incollection{citeulike:6053688, 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\"{o}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.}, author = {Bove, Ana and Dybjer, Peter and Norell, Ulf}, citeulike-article-id = {6053688}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-03359-9_6}, citeulike-linkout-1 = {http://www.springerlink.com/content/h12lq70470983732}, doi = {10.1007/978-3-642-03359-9_6}, journal = {Theorem Proving in Higher Order Logics}, keywords = {dependent-types, language-agda, reflection-proof}, pages = {73--78}, posted-at = {2009-11-01 17:02:39}, priority = {0}, title = {A Brief Overview of Agda – A Functional Language with Dependent Types}, url = {http://dx.doi.org/10.1007/978-3-642-03359-9_6}, year = {2009} }

TY - CHAP ID - citeulike:6053688 L3 - citeulike-article-id:6053688 N2 - 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. JF - Theorem Proving in Higher Order Logics EP - 78 TI - A Brief Overview of Agda – A Functional Language with Dependent Types SP - 73 KW - dependent-types KW - language-agda KW - reflection-proof AU - Bove, Ana AU - Dybjer, Peter AU - Norell, Ulf PY - 2009/// UR - http://dx.doi.org/10.1007/978-3-642-03359-9_6 ER -