Programming Language
Agda Appeared 2007
Dependently typed functional programming language and proof assistant, originally developed at Chalmers University of Technology. It is used for writing and verifying proofs using a functional style, and it uniquely integrates programming and proving without a separate tactic language. Agda employs rich type systems such as dependent types, supporting inductive families and parameterized modules.
Trends languish rank #217 languish — 59 periods, 2009Q2 to 2025Q2 2009Q2 2025Q2
Influence graph Influence graph for Agda: 30 influencing languages, 0 family links C++ influenced Ada Eiffel influenced Ada Pascal influenced Ada Coq influenced Agda Haskell influenced Agda C influenced AWK sed influenced AWK Fortran influenced BASIC Fortran influenced C Ada influenced C++ APL influenced C++ C influenced C++ F# influenced C++ Haskell influenced Clean Haskell influenced CoffeeScript JavaScript influenced CoffeeScript Perl influenced CoffeeScript Python influenced CoffeeScript Ruby influenced CoffeeScript OCaml influenced Coq Ada influenced Eiffel Haskell influenced F# OCaml influenced F# Python influenced F# Standard ML influenced F# Clean influenced Haskell Lisp influenced Haskell R5RS influenced Haskell Raku influenced Haskell Scheme influenced Haskell Standard ML influenced Haskell C++ influenced Java AWK influenced JavaScript C influenced JavaScript Java influenced JavaScript Lisp influenced JavaScript Lua influenced JavaScript MoonScript influenced JavaScript Perl influenced JavaScript Python influenced JavaScript R5RS influenced JavaScript Scheme influenced JavaScript Self influenced JavaScript AWK influenced Lua C influenced Lua C++ influenced Lua Lisp influenced Lua R5RS influenced Lua Scheme influenced Lua Self influenced Lua C++ influenced MoonScript CoffeeScript influenced MoonScript Lua influenced MoonScript Scheme influenced MoonScript C influenced OCaml Pascal influenced OCaml Standard ML influenced OCaml AWK influenced Perl BASIC influenced Perl C influenced Perl C++ influenced Perl Lisp influenced Perl Raku influenced Perl sed influenced Perl Ada influenced Python APL influenced Python C influenced Python C++ influenced Python Haskell influenced Python Lisp influenced Python Perl influenced Python R5RS influenced Python Scheme influenced Python Standard ML influenced Python Lisp influenced R5RS Haskell influenced Raku JavaScript influenced Raku Perl influenced Raku Ruby influenced Raku BASIC influenced Ruby C++ influenced Ruby Eiffel influenced Ruby Lisp influenced Ruby Lua influenced Ruby MoonScript influenced Ruby Perl influenced Ruby Python influenced Ruby R5RS influenced Ruby Scheme influenced Ruby Smalltalk influenced Ruby Lisp influenced Scheme APL influenced Self Pascal influenced Standard ML Fortran sed C Pascal Eiffel BASIC Lisp AWK Ada Standard ML APL Perl R5RS Scheme OCaml Python F# C++ Self Lua Smalltalk Ruby CoffeeScript Java MoonScript JavaScript Raku Clean Coq Haskell Agda Solid arrows: influence, oldest at the top. Dashed: compiles to / is a dialect of / implements. 