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
- Module system
- (allowing "ambiguous" names that have the same definitions, etc.)
- Inductive Families
- Uniqueness of identity proofs (inductive families).
Edit | History | Recent Changes (all) | Search
Page last modified on September 25, 2007, at 12:55 PM
Powered by PmWiki