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. Bucalo
Primo
;
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.
Settore INF/01 - Informatica
Article (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/14408
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 24
  • ???jsp.display-item.citation.isi??? 19
social impact