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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
