Abstract syntax

From The Twelf Project
Jump to: navigation, search

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.


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:



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))

See also

Higher-order abstract syntax