Paper: Second-Order and Dependently-Sorted Abstract Syntax (at LICS 2008)

Authors: Marcelo P. Fiore

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.

BibTeX

  @InProceedings{Fiore-SecondOrderandDepen,
    author = 	 {Marcelo P. Fiore},
    title = 	 {Second-Order and Dependently-Sorted Abstract Syntax},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {57--68},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }