We will have an Agda language review at Chalmers on Wed Sep 26, 2007.

The review focuses on

  • the language, not libraries/applications.
  • existing features, not open-ended feature requests.
  • the language specification, not implementation details (bugs).
  • concrete issues based on experience with the Agda implementation.

Issues which may be discussed (please add more suggestions here, and make existing points more concrete):

Implicit syntax
Visibility and evaluation
(abstract keyword, etc.)
Module system
(allowing "ambiguous" names that have the same definitions, etc.)
Inductive Families
Uniqueness of identity proofs (inductive families).
Page last modified on September 25, 2007, at 12:55 PM
Powered by PmWiki