Categorical Models of Explicit Substitutions Export

@inproceedings{citeulike:401389, abstract = {This paper concerns itself with the categorical semantics of -calculi extended with explicit substitutions. For the simply-typed -calculus, indexed categories seem to provide the right categorical framework but because these structures are inherently non-linear, alternate models are needed for linear -calculi extended with explicit substitutions. We propose to replace indexed categories by presheaves and obtain a semantics which can be specialised to both the linear and the intuitionistic...}, author = {Ghani, Neil and de Paiva, Valeria and Ritter, Eike}, booktitle = {Foundations of Software Science and Computation Structure}, citeulike-article-id = {401389}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.9308}, keywords = {categorical, explicit-subs, own}, pages = {197--211}, posted-at = {2005-11-19 17:13:25}, priority = {0}, title = {Categorical Models of Explicit Substitutions}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.9308}, year = {1999} }

TY - CONF ID - citeulike:401389 L3 - citeulike-article-id:401389 N2 - This paper concerns itself with the categorical semantics of -calculi extended with explicit substitutions. For the simply-typed -calculus, indexed categories seem to provide the right categorical framework but because these structures are inherently non-linear, alternate models are needed for linear -calculi extended with explicit substitutions. We propose to replace indexed categories by presheaves and obtain a semantics which can be specialised to both the linear and the intuitionistic... EP - 211 TI - Categorical Models of Explicit Substitutions T2 - Foundations of Software Science and Computation Structure SP - 197 KW - categorical KW - explicit-subs KW - own AU - Ghani, Neil AU - de Paiva, Valeria AU - Ritter, Eike PY - 1999/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.9308 ER -