Representing Structural Language Features in Formal Meta-languages

Müller D, Rabe F, Rothgang C, Kohlhase M (2020)

Publication Language: English

Publication Type: Conference contribution, Original article

Publication year: 2020

Publisher: Springer

Pages Range: 206 - 221

Conference Proceedings Title: Lecture Notes in Computer Science, vol 12236

Event location: Bertinoro IT

ISBN: 978-3-030-53517-9

DOI: 10.1007/978-3-030-53518-6_13

Open Access Link: https://link.springer.com/content/pdf/10.1007/978-3-030-53518-6_13.pdf

Abstract

Structural language features are those that introduce new kinds of declarations as opposed to those that only add expressions. They pose a significant challenge when representing languages in meta-languages such as standard formats like OMDoc or logical frameworks like LF. It is desirable to use shallow representations where a structural language feature is represented by the analogous feature of the meta-language, but the richness of structural language features in practical languages makes this difficult. Therefore, the current state of the art is to encode unrepresentable structural language features in terms of more elementary ones, but that makes the representations difficult to reuse and verify. This challenge is exacerbated by the fact that many languages allow users to add new structural language features that are elaborated into a small trusted kernel, which allows for a large and growing set of features. In this paper we extend the MMT representation framework with a generic concept of structural features. This allows defining exactly the language features needed for elegant shallow embeddings of object languages. The key achievement here is to make this concept expressive enough to cover complex practical features while retaining the simplicity of existing meta-languages. We exemplify our framework with representations of various important structural features including datatype definitions and theory instantiations.

Authors with CRIS profile

Dennis Müller Professur für Wissensrepräsentation und -verarbeitung Florian Rabe Professur für Wissensrepräsentation und -verarbeitung Colin Rothgang Professur für Wissensrepräsentation und -verarbeitung Michael Kohlhase Professur für Wissensrepräsentation und -verarbeitung

How to cite

APA:

Müller, D., Rabe, F., Rothgang, C., & Kohlhase, M. (2020). Representing Structural Language Features in Formal Meta-languages. In Springer (Eds.), Lecture Notes in Computer Science, vol 12236 (pp. 206 - 221). Bertinoro, IT: Springer.

MLA:

Müller, Dennis, et al. "Representing Structural Language Features in Formal Meta-languages." Proceedings of the The 13th Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro Ed. Springer, Springer, 2020. 206 - 221.

BibTeX: Download