Initial semantics in logics with constructors

Daniel Gəinə, Kokichi Futatsugi

Research output: Contribution to journalArticlepeer-review

13 Citations (Scopus)


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
Issue number1
Publication statusPublished - Sept 30 2015
Externally publishedYes

All Science Journal Classification (ASJC) codes

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


Dive into the research topics of 'Initial semantics in logics with constructors'. Together they form a unique fingerprint.

Cite this