The proposition-as-types correspondence applied to first-order log- ical theories and the associated type systems says that they are different al- though equivalent presentations of the same entity. But the nature of this entity is not clear, as these system are interpreted in distinct categories and in different ways. In this contribution, an alternative framework is introduced so that the interpretations of the logical system and of the type theory identify the same entity, which acquires both a logical and a computational meaning at the semantic level. It is shown that this semantics is sound and complete, both in the logical and in the type-theoretic sense. Also, it is shown that the standard models for interpreting first-order systems in category theory can be transformed in equivalent models in the presented framework.

Proof-Oriented Categorical Semantics

BENINI, MARCO
2016-01-01

Abstract

The proposition-as-types correspondence applied to first-order log- ical theories and the associated type systems says that they are different al- though equivalent presentations of the same entity. But the nature of this entity is not clear, as these system are interpreted in distinct categories and in different ways. In this contribution, an alternative framework is introduced so that the interpretations of the logical system and of the type theory identify the same entity, which acquires both a logical and a computational meaning at the semantic level. It is shown that this semantics is sound and complete, both in the logical and in the type-theoretic sense. Also, it is shown that the standard models for interpreting first-order systems in category theory can be transformed in equivalent models in the presented framework.
2016
De Gruyter
9781501502620
9781501510809
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11383/2044808
 Attenzione

L'Ateneo sottopone a validazione solo i file PDF allegati

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact