Logic in Computer Science, Symposium on (2008)

June 24, 2008 to June 27, 2008

ISSN: 1043-6871

ISBN: 978-0-7695-3183-0

pp: 57-68

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2008.38

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.

INDEX TERMS

abstract syntax, second-order syntax, dependently-sorted syntax, alpha-equivalence, variable binding, substitution, metavariable, meta-substitution, categorical algebra

CITATION

Marcelo Fiore,
"Second-Order and Dependently-Sorted Abstract Syntax",

*Logic in Computer Science, Symposium on*, vol. 00, no. , pp. 57-68, 2008, doi:10.1109/LICS.2008.38