Back to University of Twente portal
Equational type logic
Manca, V. and Salibra, A. and Scollo, G. (1990) Equational type logic. Theoretical Computer Science, 77 (1-2). pp. 131-159. ISSN 0304-3975
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 3100Kb |
| Abstract: | Equational type logic is an extension of (conditional) equational logic, that enables one to deal in a single, unified framework with diverse phenomena such as partiality, type polymorphism and dependent types. In this logic, terms may denote types as well as elements, and atomic formulae are either equations or type assignments. Models of this logic are type algebras, viz. universal algebras equipped with a binary relation—to support type assignment. Equational type logic has a sound and complete calculus, and initial models exist. The use of equational type logic is illustrated by means of simple examples, where all of the aforementioned phenomena occur. Formal notions of reduction and extension are introduced, and their relationship to free constructions is investigated. Computational aspects of equational type logic are investigated in the framework of conditional term rewriting systems, generalizing known results on confluence of these systems. Finally, some closely related work is reviewed and future research directions are outlined in the conclusions. |
| Item Type: | Article |
| Copyright: | © 1990 Elsevier |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Research Group: | |
| Link to this item: | http://purl.utwente.nl/publications/72917 |
| Official URL: | http://dx.doi.org/10.1016/0304-3975(90)90118-2 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page
Metis ID: 118622