Abstract
Language analysis aims at establishing properties of languages, which provides strong guarantees on the behavior of every program written in such languages. Tools that automate language analysis often need to browse a language definition given as input and retrieve information from grammars, typing rules, reduction rules, and other components of the language.
In this paper, we propose a languages-as-databases approach where language definitions are stored as database tables. Our main contribution is \(\textsc {Lang-Sql}\), a SQL-inspired query language that can express queries over languages. The key characteristic of \(\textsc {Lang-Sql}\) is that it contains linguistic features that are specific to query operational semantics aspects.
To demonstrate that \(\textsc {Lang-Sql}\) can be used in practical applications, we have used \(\textsc {Lang-Sql}\) queries to rewrite the majority of \(\textsc {Lang-n-Check}\), a tool that analyzes languages and establishes their type soundness. Our queries are declarative, and concisely express complicated operations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Aceto, L., Goriac, E., Ingólfsdóttir, A.: Meta SOS - a maude based SOS meta-theory framework. In: Borgström, J., Luttik, B. (eds.) Proceedings Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics, EXPRESS/SOS 2013, Buenos Aires, Argentina, 26th August 2013. EPTCS, vol. 120, pp. 93–107 (2013). https://doi.org/10.4204/EPTCS.120.8
Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453–468. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48168-0_32
van Antwerpen, H., Bach Poulsen, C., Rouvoet, A., Visser, E.: Scopes as types. Proc. ACM Program. Lang. (PACMPL) 2(OOPSLA), 1–30 (2018). https://doi.org/10.1145/3276484
Bach Poulsen, C., Rouvoet, A., Tolmach, A., Krebbers, R., Visser, E.: Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Program. Lang. (PACMPL) 2(POPL), 1–34 (2017). https://doi.org/10.1145/3158104
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42(1), 232–268 (1995). https://doi.org/10.1145/200836.200876
Cheney, J.: Toward a general theory of names: binding and scope. In: Pollack, R. (ed.) Proceedings of the 3rd ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN 2005, pp. 33–40. Association for Computing Machinery, New York (2005). https://doi.org/10.1145/1088454.1088459
Cimini, M.: Lang-n-check. https://github.com/mcimini/TypeSoundnessCertifier (2015)
Cimini, M.: Languages as first-class citizens (vision paper). In: Pearce, D.J., Mayerhofer, T., Steimann, F. (eds.) Proceedings of the 11th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2018, pp. 65–69. Association for Computing Machinery, New York (2018). https://doi.org/10.1145/3276604.3276983
Cimini, M.: On the effectiveness of higher-order logic programming in language-oriented programming. In: Nakano, K., Sagonas, K. (eds.) FLOPS 2020. LNCS, vol. 12073, pp. 106–123. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-59025-3_7
Cimini, M.: A calculus for multi-language operational semantics. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) Software Verification. NSV VSTTE 2021 2021. Lecture Notes in Computer Science, vol. 13124, pp. 25–42. Springer (2021). https://doi.org/10.1007/978-3-030-95561-8_3
Cimini, M.: Example of language in lang-SQL. https://github.com/mcimini/lang-sql/blob/main/Lang-n-Check/languages/stlc_cbv.lan (2022)
Cimini, M.: Lang-SQL. https://github.com/mcimini/lang-sql (2022)
Cimini, M., Miller, D., Siek, J.G.: Extrinsically typed operational semantics for functional languages. In: Lämmel, R., Tratt, L., de Lara, J. (eds.) Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, November 16–17 2020, pp. 108–125. ACM (2020). https://doi.org/10.1145/3426425.3426936
Grewe, S., Erdweg, S., Mezini, M.: Using vampire in soundness proofs of type systems. In: Kovács, L., Voronkov, A. (eds.) Proceedings of the 1st and 2nd Vampire Workshops. EPiC Series in Computing, vol. 38, pp. 33–51. EasyChair (2016). https://doi.org/10.29007/22x6
Grewe, S., Erdweg, S., Mezini, M.: Automating proof steps of progress proofs: comparing vampire and Dafny. In: Kovács, L., Voronkov, A. (eds.) Vampire 2016. Proceedings of the 3rd Vampire Workshop. EPiC Series in Computing, vol. 44, pp. 33–45. EasyChair (2017). https://doi.org/10.29007/5zjp
Grewe, S., Erdweg, S., Wittmann, P., Mezini, M.: Type systems for the masses: deriving soundness proofs and efficient checkers. In: Murphy, G.C., Steele Jr., G.L. (eds.) 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), pp. 137–150. Onward! 2015, ACM, New York (2015). https://doi.org/10.1145/2814228.2814239
Harper, R.: Practical Foundations for Programming Languages, 2nd edn. Cambridge University Press, Cambridge (2016). https://doi.org/10.1017/CBO9781316576892
Mousavi, M.R., Reniers, M.A.: Prototyping SOS meta-theory in Maude. Electron. Notes . Theor. Comput. Sci. 156(1), 135–150 (2006). https://doi.org/10.1016/j.entcs.2005.09.030
Mousavi, M.R., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theor. Comput. Sci. 373(3), 238–272 (2007). https://doi.org/10.1016/j.tcs.2006.12.019
Neron, P., Tolmach, A., Visser, E., Wachsmuth, G.: A theory of name resolution. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 205–231. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46669-8_9
Roberson, M., Harries, M., Darga, P.T., Boyapati, C.: Efficient software model checking of soundness of type systems. In: Harris, G.E. (ed.) Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, pp. 493–504. OOPSLA 2008, Association for Computing Machinery, New York (2008). https://doi.org/10.1145/1449764.1449803
Rouvoet, A., Bach Poulsen, C., Krebbers, R., Visser, E.: Intrinsically-typed definitional interpreters for linear, session-typed languages. In: Blanchette, J., Hritcu, C. (eds.) Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21 2020, pp. 284–298. ACM (2020). https://doi.org/10.1145/3372885.3373818
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Cimini, M. (2022). A Query Language for Language Analysis. In: Schlingloff, BH., Chai, M. (eds) Software Engineering and Formal Methods. SEFM 2022. Lecture Notes in Computer Science, vol 13550. Springer, Cham. https://doi.org/10.1007/978-3-031-17108-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-031-17108-6_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-17107-9
Online ISBN: 978-3-031-17108-6
eBook Packages: Computer ScienceComputer Science (R0)