A Framework for Typed HOAS and Semantics

We investigate a framework for representing and reasoning about syntactic and semantic aspects of typed languages with variable binders.First, we introduce typed binding signatures and develop a theory of typed abstract syntax with binders. Each signature is associated to a category of "presentation" models, where the language of the typed signature is the initial model.At the semantic level, types can be given also a computational meaning in a (possibly different) semantic category. We observe that in general, semantic aspects of terms and variables can be reflected in the presentation category by means of an adjunction. Therefore, the category of presentation models is expressive enough to represent both the syntactic and the semantic aspects of languages.We introduce then a metalogical system, inspired by the internal languages of the presentation category, which can be used for reasoning on both the syntax and the semantics of languages. This system is composed by a core equational logic tailored for reasoning on the syntactic aspects; when a specific semantics is chosen, the system can be modularly extended with further "semantic" notions, as needed.