Initial semantics in logics with constructors

Daniel Gəinə, Kokichi Futatsugi

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

The constructor-based logics constitute the logical foundation of the so-called OTS/CafeOBJ method, a modelling, specification and verification method of the observational transition systems. The important role played in algebraic specifications by the initial algebras semantics is well known. Free models along presentation morphisms provide semantics for the modules with initial denotation in structured specification languages. Following Goguen and Burstall, the notion of logical system over which we build specifications is formalized as an institution. The present work is an institution-independent study of the existence of free models along sufficient complete presentation morphisms in logics with constructors in the signatures.

Original languageEnglish
Pages (from-to)95-116
Number of pages22
JournalJournal of Logic and Computation
Volume25
Issue number1
DOIs
Publication statusPublished - Sep 30 2015
Externally publishedYes

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture
  • Logic

Cite this