Paper: Type Theory via Exact Categories (at LICS 1998)
Authors: Lars Birkedal Aurelio Carboni Giuseppe Rosolini Dana S. Scott
Abstract
Partial equivalence relations (and categories of these) are a standard tool in semantics of type theories and programming languages, since they often provide a cartesian closed category with extended definability. Using the theory of exact categories, we give a category-theoretic explanation of why the construction of a category of partial equivalence relations often produces a cartesian closed category. We show how several familiar examples of categories of partial equivalence relations fit into the general framework
BibTeX
@InProceedings{BirkedalCarboniRoso-TypeTheoryviaExactC, author = {Lars Birkedal and Aurelio Carboni and Giuseppe Rosolini and Dana S. Scott}, title = {Type Theory via Exact Categories}, booktitle = {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)}, year = {1998}, month = {June}, pages = {188--198}, location = {Indianapolis, IN, USA}, publisher = {IEEE Computer Society Press} }