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

open access
PDF - Published Version
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
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/72917
Official URL:https://doi.org/10.1016/0304-3975(90)90118-2
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 118622