First, we briefly recall the main definitions of the theory of Information Bases and Translations. These mathematical structures are the basis to construct the cartesian closed category InfBas, which is equivalent to the category ScDom of Scott domains. Then, we will show that all the definitions and the proof of all the properties that one needs in order to show that InfBas is indeed a cartesian closed category can be formalized within Martin-Löf's intuitionistic type theory.

A cartesian closed category in Martin-Loef's intuitionistic type theory

VALENTINI, SILVIO
2003

Abstract

First, we briefly recall the main definitions of the theory of Information Bases and Translations. These mathematical structures are the basis to construct the cartesian closed category InfBas, which is equivalent to the category ScDom of Scott domains. Then, we will show that all the definitions and the proof of all the properties that one needs in order to show that InfBas is indeed a cartesian closed category can be formalized within Martin-Löf's intuitionistic type theory.
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/11577/1373647
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 2
  • OpenAlex ND
social impact