One of the problems of computer languages comes from the fact that one (a human or a compiler) has to connect the uses of identifiers with their definitions. This problem is known as the binding problem, with a myriad of variants or related topics: scope of declarations, visibility of a variable, nesting of environments, visibility holes, capture of variables, substitutions rules, etc.
The need to incorporate the notion of binding into abstract
syntaxes leads to what is called higher-order abstract
syntax. Higher-order abstract syntax has already been used in some
systems as 
-Prolog [10, 11] or Elf
[12] and some experiments of defining or implementing
the semantics of computer formalisms has been made
[6]. However, no system has integrated this notion to
produce complete programming environments. AS will integrate the
notion of higher-order abstract syntax, restricted to the second-order
case that seems sufficient for most of practical applications.
Note that if some languages
(derived for example from the simply typed -calculus) have an
obvious binding rule (let's say that bindings can be decided at parse
time), this is not the case for some other ones in which bindings can
only be made after type-checking. This is the case for example for
Pascal (due to the ``with'' construction), or for ADA (due to
overloading). For this reason, AS will provide a way to define at the
same time a first-order an a second-order abstract syntax for the same
formalism.
Thierry Despeyroux