Equational type logic

V. Manca, A. Salibra, Giuseppe Scollo

    Research output: Contribution to journalArticleAcademicpeer-review

    33 Citations (Scopus)
    141 Downloads (Pure)


    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.
    Original languageEnglish
    Pages (from-to)131-159
    Number of pages19
    JournalTheoretical computer science
    Issue number1-2
    Publication statusPublished - 1990


    • METIS-118622
    • IR-72917


    Dive into the research topics of 'Equational type logic'. Together they form a unique fingerprint.

    Cite this