The Theory of Contexts is a type-theoretic axiomatization which has been recently proposed by some of the authors for giving 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 the model validates Classical Higher Order Logic, The Theory of Contexts, and also (parametrised) structural induction and recursion principles over contexts. The approach we present in full detail should be useful also for reasoning on other models based on functor categories. Moreover, the construction could be adopted, and possibly generalized, also for validating other theories of names and binders.
Consistency of The Theory of Contexts / A. Bucalo, M. Hofmann, F. Honsell, M. Miculan, I. Scagnetto. - In: JOURNAL OF FUNCTIONAL PROGRAMMING. - ISSN 0956-7968. - 16:3(2006 May), pp. 327-395. [10.1017/S0956796806005892]
Consistency of The Theory of Contexts
A. BucaloPrimo
;
2006
Abstract
The Theory of Contexts is a type-theoretic axiomatization which has been recently proposed by some of the authors for giving 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 the model validates Classical Higher Order Logic, The Theory of Contexts, and also (parametrised) structural induction and recursion principles over contexts. The approach we present in full detail should be useful also for reasoning on other models based on functor categories. Moreover, the construction could be adopted, and possibly generalized, also for validating other theories of names and binders.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.