Abstract syntax
The abstract syntax of a programming language is an unambiguous representation of the syntax of a language; most compilers and most language definitions work in terms of the abstract syntax of a language as opposed to the concrete syntax of a language, which is what the programmer actually writes down. Twelf can encode the abstract syntax of a language, and can furthermore gracefully encode the idea of binding by using higher-order abstract syntax.
Example
The concrete syntax of a simple language might look like this:
if 1 = 2 then 1 + if true then 3 else 6 else 6
and the abstract syntax in a language like ML might look like this:
If(Eq(Num(1),Num(2)),
Plus(Num(1),If(True,Num(3),Num(6))), Num(6))
and the same abstract syntax in a language like Twelf might look like this:
(if (eq (num 1) (num 2))
(plus (num 1) (if true (num 3) (num 6))) (num 6))
