  Despite extensive research both on the theoretical and practical fronts,
formalising, reasoning about, and implementing languages with variable binding
is still a daunting endeavour - repetitive boilerplate and the overly
complicated metatheory of capture-avoiding substitution often get in the way of
progressing on to the actually interesting properties of a language. Existing
developments offer some relief, however at the expense of inconvenient and
error-prone term encodings and lack of formal foundations.
  We present a mathematically-inspired language-formalisation framework
implemented in Agda. The system translates the description of a syntax
signature with variable-binding operators into an intrinsically-encoded,
inductive data type equipped with syntactic operations such as weakening and
substitution, along with their correctness properties. The generated metatheory
further incorporates metavariables and their associated operation of
metasubstitution, which enables second-order equational/rewriting reasoning.
The underlying mathematical foundation of the framework - initial algebra
semantics - derives compositional interpretations of languages into their
models satisfying the semantic substitution lemma by construction.
