by Lutz Schröder
Abstract:
We investigate the logical aspects of the partial lambda-calculus with equality, exploiting an equivalence between partial lambda-theories and partial cartesian closed categories (pcccs) established here. The partial lambda-calculus with equality provides a full-blown intuitionistic higher order logic, which in a precise sense turns out to be almost the logic of toposes, the distinctive feature of the latter being unique choice. We give a linguistic proof of the generalization of the fundamental theorem of toposes to pcccs with equality; type theoretically, one thus obtains that the partial lambda-calculus with equality encompasses a Martin-Löf-style dependent type theory. This work forms part of the semantical foundations for the higher order algebraic specification language HasCASL.
Reference:
Lutz Schröder: The logic of the partial $\lambda$-calculus with equality, In Jerzy Marcinkowski, Andrzej Tarlecki, eds.: Computer Science Logic (CSL 04), Lecture Notes in Computer Science, vol. 3210, pp. 385–399, Springer; Berlin; http://www.springer.de, 2004. [preprint]
Bibtex Entry:
@InProceedings{Schroder04,
author = {Lutz Schr{\"o}der},
title = {The logic of the partial {$\lambda$}-calculus with equality},
year = {2004},
editor = {Jerzy Marcinkowski and Andrzej Tarlecki},
booktitle = {Computer Science Logic (CSL 04)},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
volume = {3210},
pages = {385--399},
keywords = {Partial lambda-calculus partial cartesian closed category HasCASL dependent type topos},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3210&spage=385},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/deptypes.pdf"> [preprint] </a>},
psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/deptypes.ps},
abstract = {We investigate the logical aspects of the partial lambda-calculus
with equality, exploiting an equivalence between partial
lambda-theories and partial cartesian closed categories (pcccs)
established here. The partial lambda-calculus with equality provides a full-blown intuitionistic higher order logic, which in a precise sense turns out to be almost the logic of toposes, the distinctive feature of the latter being unique choice. We give a linguistic proof of the generalization of the fundamental theorem of toposes to pcccs with equality; type theoretically, one thus obtains that the partial lambda-calculus with equality encompasses a Martin-L{\"o}f-style dependent type theory. This work forms part of the semantical foundations for the higher order algebraic specification language HasCASL.
},
}