Open Access

Feryal Fulya Horozal

• Declarative languages are an important family of formalisms used for formal knowledge representation in computer science. Examples include logics, type theories, set theories, specification languages and ontology languages. Despite the vast variety of declarative languages, they share a common structure: A possibly infinite collection of theories, which are sets of declarations, and a set of well-formed expressions over each theory. This PhD thesis contributes to the design of declarative logical frameworks that balances the trade-off between abstract and concrete representations of declarative languages. In particular, we identify a new feature that can be added to a declarative framework as a language primitive: declaration patterns. The main idea behind this feature is to capture the common structure of the theories of declarative languages. More specifically, we reify declaration patterns as a language primitive for declarative logical frameworks and use them to characterize the legal declarations of non-logical symbols by specifying their syntactic shape. Then, we introduce a notion of pattern-based translation, which maps legal theories of one declarative language to legal theories of the other language. We introduce these novel notions in a calculus-based meta-framework for defining declarative languages and translations between them. Our meta-framework is independent of the underlying declarative logical framework and can be instantiated with specific logical frameworks like LF. In particular we develop a new declarative logical framework LFS (LF with sequences) that supports sequences and dependent function spaces that take sequence arguments, which we need for writing down the declaration patterns of most declarative languages. We apply and evaluate our pattern-based approach in an atlas of declarative languages, which includes various logics ranging from traditional first-order logic to more complex languages such as polymorphic higher order logic.