| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Lutz Schröder |
| Herausgeber: |
Jerzy Marcinkowski, Andrzej Tarlecki |
| Titel: |
The logic of the partial λ-calculus with equality |
| Buch / Sammlungs-Titel: |
Computer Science Logic (CSL 04) |
| Band: |
3210 |
| Seite(n): |
385 – 399 |
| Serie / Reihe: |
Lecture Notes in Computer Science |
| Erscheinungsjahr: |
2004 |
| Verleger: |
Springer, Berlin |
| Abstract / Kurzbeschreibung: |
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.
|
| Internet: |
http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3210&spage=385 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/deptypes.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/deptypes.ps |
| Schlagworte: |
Partial lambda-calculus partial cartesian closed category HasCASL dependent type topos |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
22. 06. 2005 |
