Second-Order and Dependently-Sorted Abstract Syntax

Abstract

The paper develops a mathematical theory in the spirit of categorical algebra that provides a model theory for second-order and dependently-sorted syntax. The theory embodies notions such as alpha-equivalence, variable binding, capture-avoiding simultaneous substitution, term metavariable, meta-substitution, mono and multi sorting, and sort dependency. As a matter of illustration, a model is used to extract a second-order syntactic theory, which is thus guaranteed to be correct by construction.