Daniel Găină
My primary research interest lies in universal logic, which aims to develop general frameworks for constructing and reasoning about a wide variety of logical systems. Within this paradigm, I focus on institution model theory, a category-based formalization of the informal notion of logical systems, which includes signatures, sentences, models, and satisfaction relations. By leveraging the expressive power of category theory, institution model theory provides a unified and abstract treatment of logic, enabling systematic comparison, integration, and interoperability among diverse logical systems.
Following my graduation, I contributed to the design of CafeOBJ, an algebraic specification language developed at the Japan Advanced Institute of Science and Technology with substantial support from the Japanese government. A central goal of this work was to establish a rigorous logical foundation for proof scores, a formal method that supports both the specification of software systems and their structured, interactive verification.
Building on this foundation, I designed the Constructor-based Inductive Theorem Prover (CITP) , which supports inductive reasoning over algebraic specifications within an institutional framework. To enhance the logical expressiveness of CITP, I introduced transition algebra — a many-sorted first-order logic extended with dynamic logic features, including state transitions, their composition, union, and reflexive-transitive closure.
