Agda swMATH ID: 9689 Software Authors: Ulf Norell Description: Agda is a dependently typed functional programming language: It has inductive families, which are similar to Haskell’s GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code). Agda is also a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. This package includes both a command-line program (agda) and an Emacs mode. If you want to use the Emacs mode you can set it up by running agda-mode setup (see the README). Note that the Agda library does not follow the package versioning policy, because it is not intended to be used by third-party packages. Homepage: http://wiki.portal.chalmers.se/agda/pmwiki.php Related Software: Coq; Haskell; HOL Light; Isabelle/HOL; Nuprl; Idris; Lean; Isabelle; HOL; GitHub; Mizar; Matita; PVS; Twelf; Irdis; ML; Epigram; Automath; AoPA; Abella Referenced in: 208 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Dependently typed programming in Agda. Zbl 1263.68038Norell, Ulf 2009 all top 5 Referenced by 279 Authors 13 Abel, Andreas M. 11 Uustalu, Tarmo 8 Chapman, James T. E. 7 Altenkirch, Thorsten 7 Dybjer, Peter 7 Farmer, William M. 7 Setzer, Anton 6 Devriese, Dominique 6 Popescu, Andrei 6 Swierstra, Wouter 5 Carette, Jacques 5 Cockx, Jesper 5 Danielsson, Nils Anders 5 Kahl, Wolfram 5 Piessens, Frank 5 Rahli, Vincent 4 Bickford, Mark 4 Bove, Ana 4 Coquand, Thierry 4 Hötzel Escardó, Martín 4 Jansson, Patrik 4 Kunčar, Ondřej 4 Mu, Shin-Cheng 4 Pientka, Brigitte 4 Veltri, Niccolò 4 Weirich, Stephanie 3 Berger, Ulrich 3 Brady, Edwin C. 3 Capretta, Venanzio 3 Cohen, Liron 3 Firsov, Denis 3 Kraus, Nicolai 3 Licata, Daniel R. 3 Michelbrink, Markus 3 Miller, Dale Allen 3 Pouillard, Nicolas 3 Rabe, Florian 3 Sozeau, Matthieu 3 Vezzosi, Andrea 3 Wadler, Philip Lee 3 Wiedijk, Freek 3 Xu, Chuangjie 2 Ahman, Danel 2 Blanchette, Jasmin Christian 2 Botta, Nicola 2 Buchholtz, Ulrik 2 Capriotti, Paolo 2 Casinghino, Chris 2 Constable, Robert Lee 2 Copello, Ernesto 2 Daggitt, Matthew L. 2 de Moura, Leonardo 2 Griffin, Timothy G. 2 Ionescu, Cezar 2 Kaliszyk, Cezary 2 Ko, Hsiang-Shang 2 Komendantskaya, Ekaterina 2 Koopman, Pieter 2 Lawrence, Andrew 2 Libal, Tomer 2 Lindblad, Fredrik 2 Löh, Andres 2 Luo, Zhaohui 2 McBride, Conor Thomas 2 Meshveliani, S. D. 2 Møgelberg, Rasmus Ejlers 2 Nordvall Forsberg, Fredrik 2 Norell, Ulf 2 Pottier, François 2 Sacerdoti Coen, Claudio 2 Schubert, Aleksy 2 Sculthorpe, Neil 2 Seisenberger, Monika 2 Sharoda, Yasmine 2 Siek, Jeremy G. 2 Sjöberg, Vilhelm 2 Szasz, Nora 2 Tasistro, Alvaro 2 Tassi, Enrico 2 Traytel, Dmitry 2 Urzyczyn, Paweł 2 van Doorn, Floris 2 Voigtlander, Janis 2 von Raumer, Jakob 2 Zdancewic, Steve 2 Ziliani, Beta 2 Zmigrod, Ran 1 Achten, Peter 1 Adelsberger, Stephan 1 Ahrens, Benedikt 1 Al-Sibahi, Ahmad Salim 1 Aldrich, Jonathan 1 Allais, Guillaume 1 Anand, Abhishek 1 Armstrong, Alasdair 1 Asperti, Andrea 1 Atkey, Robert 1 Avigad, Jeremy 1 Bach Poulsen, Casper 1 Bar, Krzysztof ...and 179 more Authors all top 5 Referenced in 25 Serials 23 Journal of Functional Programming 13 Logical Methods in Computer Science 9 Journal of Automated Reasoning 8 MSCS. Mathematical Structures in Computer Science 5 Theoretical Computer Science 4 Lecture Notes in Computer Science 4 Journal of Logical and Algebraic Methods in Programming 3 Annals of Pure and Applied Logic 3 Higher-Order and Symbolic Computation 3 ACM Transactions on Computational Logic 3 Journal of Formalized Reasoning 2 Programming and Computer Software 1 Artificial Intelligence 1 Journal of Symbolic Computation 1 Information and Computation 1 Formal Aspects of Computing 1 Archive for Mathematical Logic 1 Indagationes Mathematicae. New Series 1 Formal Methods in System Design 1 Journal of Mathematical Sciences (New York) 1 Advances in Applied Clifford Algebras 1 Annals of Mathematics and Artificial Intelligence 1 Journal of the ACM 1 The Journal of Logic and Algebraic Programming 1 Mathematics in Computer Science all top 5 Referenced in 16 Fields 195 Computer science (68-XX) 76 Mathematical logic and foundations (03-XX) 17 Category theory; homological algebra (18-XX) 10 Algebraic topology (55-XX) 6 General and overarching topics; collections (00-XX) 2 Combinatorics (05-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 2 General algebraic systems (08-XX) 2 Number theory (11-XX) 2 Commutative algebra (13-XX) 2 Operations research, mathematical programming (90-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Group theory and generalizations (20-XX) 1 Geometry (51-XX) 1 General topology (54-XX) Referencing Publications by Year