AgdaLight is a version of the Agda proof checker. It is much more volatile than Agda and it's main purpose is to serve as a test platform for cool new extensions that are too experimental to make it into the real system. Be warned that AgdaLight is an experimental system, features may disappear and the syntax may change without any notice. Features * Datatypes. * Definitions by pattern matching. * Implicit arguments. * First-order logic plugin. * QuickCheck plugin. * Inductive families. * Signatures and structures (+signature subtyping). * Command line interface. * Pattern completeness checking. * LaTeX compiler (great for writing papers). Not in AgdaLight * Termination checking. * Fancy emacs interface. * Module system.
The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types. 1. Epigram 2. ATS (successor to Dependent ML) 3. Agda (successor to Cayenne) 4. Ωmega 5. NuPrl 6. Twelf 7. Isabelle 8. Coq etc caveats * Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq. * Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Is it time yet to do anything about the cornucopia of options? see comments
Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system. Code accompanying the paper has been developed into an Agda library AoPA.