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

By Ana Bove, Peter Dybjer, Ulf Norell. International Conference on Theorem Proving in Higher Order Logics, 2009

302 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/5b8b75c3049b78461e1f1eab598f4cc22ff898aa

How researchers see this paper

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

In Artificial Intelligence

1. Josef Urban
2. John Harrison
3. Freek Wiedijk
4. Jia Deng

In Computational Theory and Mathematics

1. Josef Urban
2. John Harrison
3. Freek Wiedijk
4. Jia Deng

Citations in the corpus

• History of Interactive Theorem Proving (2014, methodology): “Finally Norell implemented a new version of this system in 2007 under the name of Agda2 [Bove et al., 2009].”