Dependently typed programming in Agda

By Ulf Norell. ACM SIGPLAN International Workshop on Types In Languages Design And Implementation, 2009

451 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Toward Semantic Foundations for Program Editors (2017, background): “Syntax of H-types and H-expressions in the Hazelnut calculus [37]. and the Agda proof assistant [35], support a workﬂow where the programmer places holes manually at locations in the program that remain under construction.”
A Brief Overview of Agda - A Functional Language with Dependent Types (2009, methodology): “There are tutorials [15, 3], a guide to editing, type checking, and compiling Agda code, a link to the standard library, and much else.”
Monads need not be endofunctors (2010, background): “uctions similar to monads, such as comonads [36], arrows [20] and idioms (closed functors) [25]. Indeed, especially when working in an expressive and total language with dependent types, such as Agda [27], we can exploit monads as a way to structure not only our programs but also their veriﬁcation. ”
The Lean Theorem Prover (System Description) (2015, unknown): “Finally, when proof irrelevance is enabled in the kernel, axiom K [22] “computes” in Lean (a similar feature is available in Agda [18]).”