by Lutz Schröder
Abstract:
Along the lines of classical categorical type theory for total functions, we establish correspondence results between certain classes of partial equational theories on the one hand and suitable classes of categories having certain finite limits on the other hand. E.g., we show that finitary partial theories with existentially conditioned equations are essentially the same as cartesian categories with distinguished domains, and that partial lambda-calculi with internal equality are equivalent to a suitable class of partial cartesian closed categories.
Reference:
Lutz Schröder: Classifying categories for partial equational logic, In Richard Blute, ed.: Category Theory and Computer Science (CTCS 02), Electronic Notes in Theoretical Computer Science, vol. 69, Elsevier, 2003. [preprint]
Bibtex Entry:
@InProceedings{Schroder03,
author = {Lutz Schr{\"o}der},
title = {Classifying categories for partial equational logic},
year = {2003},
editor = {Richard Blute},
booktitle = {Category Theory and Computer Science (CTCS 02)},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {69},
keywords = {dominion partial equational logic partial cartesian closed category HasCASL},
url = {http://www.elsevier.com/gej-ng/31/29/23/131/23/show/Products/notes/index.htt#017},
comment = {<a href="http://www8.informatik.uni-erlangen.de/~schroeder/papers/classcat.ps">[preprint]</a>},
abstract = {Along the lines of classical categorical type theory for total functions, we establish correspondence results between certain classes of partial equational theories on the one hand and suitable classes of categories having certain finite limits on the other hand. E.g., we show that finitary partial theories with existentially conditioned equations are essentially the same as cartesian categories with distinguished domains, and that partial lambda-calculi with internal equality are equivalent to a suitable class of partial cartesian closed categories.
},
}