Second-Order and Dependently-Sorted Abstract Syntax

Author

Fiore, Marcelo

Author_Institution

Comput. Lab., Cambridge Univ., Cambridge

fYear

2008

fDate

24-27 June 2008

Firstpage

57

Lastpage

68

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.

Keywords

category theory; computational linguistics; process algebra; sorting; categorical algebra; dependently-sorted abstract syntax; mathematical theory; model theory; second-order abstract syntax; second-order syntactic theory; Algebra; Computer science; Laboratories; Logic functions; MONOS devices; Mathematical model; Sorting; abstract syntax; alpha-equivalence; categorical algebra; dependently-sorted syntax; meta-substitution; metavariable; second-order syntax; substitution; variable binding;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 2008. LICS '08. 23rd Annual IEEE Symposium on

Conference_Location

Pittsburgh, PA

ISSN

1043-6871

Print_ISBN

978-0-7695-3183-0

Type

conf

DOI

10.1109/LICS.2008.38

Filename

4557900