CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

Invited tutorial

Ana Bove (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Ulf Norell (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Theorem Proving in Higher Order Logics Vol. 5674 (2009), LNCS, p. 73--78.
[Konferensbidrag, övrigt]

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.



Denna post skapades 2009-12-11.
CPL Pubid: 103342

 

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)

Ämnesområden

Datalogi

Chalmers infrastruktur