Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional programming language with dependent types and was developed by Ulf Norell, a post-doc at Chalmers University of Technology. Agda is based on the idea of direct manipulation of proof-term and not on tactics. The proof is a term, not a script.

PropertyValue
dbpedia-owl:thumbnail
dbpprop:abstract
  • Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional programming language with dependent types and was developed by Ulf Norell, a post-doc at Chalmers University of Technology. Agda is based on the idea of direct manipulation of proof-term and not on tactics. The proof is a term, not a script. The language has ordinary programming constructs such as data-types and case-expressions, signatures and records, let-expressions and modules. The system has an Emacs interface and a graphical interface, Alfa.
dbpprop:fileExt
  • .agda, .lagda
dbpprop:hasPhotoCollection
dbpprop:influencedBy
dbpprop:latestReleaseDate
dbpprop:latestReleaseVersion
  • 2.2.4
dbpprop:name
  • Agda
dbpprop:operatingSystem
dbpprop:paradigm
  • Functional
dbpprop:reference
dbpprop:website
dbpprop:wikiPageUsesTemplate
rdfs:comment
  • Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional programming language with dependent types and was developed by Ulf Norell, a post-doc at Chalmers University of Technology. Agda is based on the idea of direct manipulation of proof-term and not on tactics. The proof is a term, not a script.
rdfs:label
  • Agda (theorem prover)
owl:sameAs
skos:subject
foaf:depiction
foaf:homepage
foaf:page
is dbpprop:disambiguates of
is dbpprop:redirect of