Logo del repository
  1. Home
 
Opzioni

Consistency of the Theory of Contexts

BUCALO A
•
HOFMANN M
•
HONSELL F
altro
SCAGNETTO I
2006
  • journal article

Periodico
JOURNAL OF FUNCTIONAL PROGRAMMING
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.
DOI
10.1017/S0956796806005892
WOS
WOS:000238238400005
SCOPUS
2-s2.0-33646396504
Archivio
http://hdl.handle.net/11390/878308
Diritti
closed access
Soggetti
  • Axiomatization

  • Classical higher-orde...

  • Functor category

  • Higher-order abstract...

  • Model-based OPC

  • Recursions

  • Structural induction

  • Theory of Contexts

  • Functional programmin...

  • Formal logic

Scopus© citazioni
24
Data di acquisizione
Jun 2, 2022
Vedi dettagli
Web of Science© citazioni
19
Data di acquisizione
Jun 4, 2022
google-scholar
Get Involved!
  • Source Code
  • Documentation
  • Slack Channel
Make it your own

DSpace-CRIS can be extensively configured to meet your needs. Decide which information need to be collected and available with fine-grained security. Start updating the theme to match your nstitution's web identity.

Need professional help?

The original creators of DSpace-CRIS at 4Science can take your project to the next level, get in touch!

Realizzato con Software DSpace-CRIS - Estensione mantenuta e ottimizzata da 4Science

  • Impostazioni dei cookie
  • Informativa sulla privacy
  • Accordo con l'utente finale
  • Invia il tuo Feedback