Marino Miculan and Ivan Scagnetto
A framework for typed HOAS and
semantics
In Proc. 5th Int'l Conf. Principles & Practice Declarative
Programming, 2003
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.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43