Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Agda (programming language)
Summary
Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.
Agda is also a proof assistant based on the propositions-as-types paradigm, but unlike Coq, has no separate tactics language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. The system has Emacs, Atom, and VS Code interfaces but can also be run in batch mode from the command line.
Agda is based on Zhaohui Luo's unified theory of dependent types (UTT), a type theory similar to Martin-Löf type theory.
Agda is named after the Swedish song "Hönan Agda", written by Cornelis Vreeswijk, which is about a hen named Agda. This alludes to the name of the theorem prover Coq, which was named after Thierry Coquand, Catarina Coquand's husband.
The main way of defining data types in Agda is via inductive data types which are similar to algebraic data types in non-dependently typed programming languages.
Here is a definition of Peano numbers in Agda:
data N : Set where
zero : N
suc : N → N
Basically, it means that there are two ways to construct a value of type , representing a natural number. To begin, zero is a natural number, and if n is a natural number, then suc n, standing for the successor of n, is a natural number too.
Here is a definition of the "less than or equal" relation between two natural numbers:
data ≤ : N → N → Set where
z≤n : {n : N} → zero ≤ n
s≤s : {n m : N} → n ≤ m → suc n ≤ suc m
The first constructor, z≤n, corresponds to the axiom that zero is less than or equal to any natural number. The second constructor, s≤s, corresponds to an inference rule, allowing to turn a proof of n ≤ m into a proof of suc n ≤ suc m.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.