Consistency of the theory of contexts Export

@article{citeulike:5986175, abstract = {The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In this paper, we prove that this theory is consistent by building a model based on functor categories . By means of a suitable notion of forcing , we prove that this model validates Classical Higher Order Logic, the Theory of Contexts, and also (parametrised) structural induction and recursion principles over contexts. Our approach, which we present in full detail, should also be useful for reasoning on other models based on functor categories. Moreover, the construction could also be adopted, and possibly generalized, for validating other theories of names and binders.}, address = {New York, NY, USA}, author = {Bucalo, Anna and Honsell, Furio and Miculan, Marino and Scagnetto, Ivan and Hoffman, Martin}, citeulike-article-id = {5986175}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1132894}, citeulike-linkout-1 = {http://dx.doi.org/10.1017/S0956796806005892}, doi = {10.1017/S0956796806005892}, issn = {0956-7968}, journal = {J. Funct. Program.}, keywords = {contexts, logic, pl}, number = {3}, pages = {327--395}, posted-at = {2009-10-22 18:50:23}, priority = {2}, publisher = {Cambridge University Press}, title = {Consistency of the theory of contexts}, url = {http://dx.doi.org/10.1017/S0956796806005892}, volume = {16}, year = {2006} }

TY - JOUR ID - citeulike:5986175 L3 - citeulike-article-id:5986175 N2 - The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In this paper, we prove that this theory is consistent by building a model based on functor categories . By means of a suitable notion of forcing , we prove that this model validates Classical Higher Order Logic, the Theory of Contexts, and also (parametrised) structural induction and recursion principles over contexts. Our approach, which we present in full detail, should also be useful for reasoning on other models based on functor categories. Moreover, the construction could also be adopted, and possibly generalized, for validating other theories of names and binders. IS - 3 JF - J. Funct. Program. SN - 0956-7968 AD - New York, NY, USA EP - 395 TI - Consistency of the theory of contexts PB - Cambridge University Press VL - 16 SP - 327 KW - contexts KW - logic KW - pl AU - Bucalo, Anna AU - Honsell, Furio AU - Miculan, Marino AU - Scagnetto, Ivan AU - Hoffman, Martin PY - 2006/// UR - http://dx.doi.org/10.1017/S0956796806005892 ER -