General structure BNF: string -> concrete syntax scope analysis: concrete syntax -> abstract syntax type checking: abstract syntax -> stack of values/value types only the last declared constant can be given a definition all declared constants are unique. Information checked for scope: identifier declared what it is number of parameters for a data type check of constructors and completness of definition of functions Possible extensions: it seems likely that the module system of Agda 2 should be incorporated in the core at a more basic level. It seems to be needed for a good treatment of constructors moduleList (A:Set) = list : Set nil : list cons : A -> list -> list append : list -> list -> list .... One can add a value for modules The value should be [Val],[Val] The type is?? One accesses the value and the value type by de Bruijn index Possible syntax (m e1 ... en).x