Affordable Access

Publisher Website

A cartesian closed category in Martin-Löf's intuitionistic type theory

Authors
Journal
Theoretical Computer Science
0304-3975
Publisher
Elsevier
Publication Date
Volume
290
Issue
1
Identifiers
DOI: 10.1016/s0304-3975(01)00309-7
Keywords
  • Intuitionistic Type Theory
  • Cartesian Closed Categories
  • Scott Domains
Disciplines
  • Mathematics

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.