Abstract
We present \(\lambda ^{{\mathrm {\mathcal {L}}}}\), a statically typed lambda-calculus with languages as first-class citizens. In \(\lambda ^{{\mathrm {\mathcal {L}}}}\), languages can be defined and used to execute programs and, furthermore, they also can be bound to variables, passed to functions, and returned by functions, among other operations. Moreover, code of different languages can safely interact thanks to pre- and post-conditions that are checked at run-time.
We provide a type system and an operational semantics for \(\lambda ^{{\mathrm {\mathcal {L}}}}\). We observe that Milner’s type safety is too strong a property in this context, as programmers may intentionally execute unsafe languages. We then identify a type safety theorem that is specific to the domain of multi-language programming, and we prove that \(\lambda ^{{\mathrm {\mathcal {L}}}}\) satisfies this theorem.
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
Notes
- 1.
Substitution operations such as e[v/x] are used in reduction rules, and not in the plain programs that programmers write.
References
van Antwerpen, H., Bach Poulsen, C., Rouvoet, A., Visser, E.: Scopes as types. Proc. ACM Program. Lang. (PACMPL) 2(OOPSLA) (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) (2017). https://doi.org/10.1145/3158104
Bousse, E., Degueule, T., Vojtisek, D., Mayerhofer, T., Deantoni, J., Combemale, B.: Execution framework of the GEMOC studio (tool demo). In: Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language Engineering, SLE 2016, pp. 84–89. Association for Computing Machinery, New York (2016). https://doi.org/10.1145/2997364.2997384
Chang, S., Knauth, A., Greenman, B.: Type systems as macros. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 694–705. Association for Computing Machinery, New York (2017). https://doi.org/10.1145/3009837.3009886
Cheney, J.: Toward a general theory of names: binding and scope. In: 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.: Languages as first-class citizens (vision paper). In: 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 (additional material) (2021). http://www.cimini.info/MultiLangCalculus/additionalMaterial.pdf
Cimini, M., Miller, D., Siek, J.G.: Extrinsically typed operational semantics for functional languages. In: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, 16–17 November 2020, pp. 108–125. Association for Computing Machinery, New York (2020). https://doi.org/10.1145/3426425.3426936
Erdweg, S., Rendel, T., Kästner, C., Ostermann, K.: SugarJ: library-based syntactic language extensibility. In: Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2011, pp. 391–406. Association for Computing Machinery, New York (2011). https://doi.org/10.1145/2048066.2048099
Erdweg, S., Rieger, F., Rendel, T., Ostermann, K.: Layout-sensitive language extensibility with SugarHaskell. In: Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Haskell 2012, Copenhagen, Denmark, 13 September 2012, pp. 149–160 (2012). https://doi.org/10.1145/2364506.2364526
Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex, 1st edn. The MIT Press, Cambridge (2009)
Flatt, M.: PLT: reference: racket. Technical report PLT-TR-2010-1, PLT Design Inc. (2010). https://racket-lang.org/tr1/
Fowler, M.: Language workbenches: the killer-app for domain specific languages? (2005). http://www.martinfowler.com/articles/languageWorkbench.html
Grewe, S., Erdweg, S., Wittmann, P., Mezini, M.: Type systems for the masses: deriving soundness proofs and efficient checkers. In: 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), Onward! 2015, pp. 137–150. ACM, New York (2015). https://doi.org/10.1145/2814228.2814239
Klint, P., van der Storm, T., Vinju, J.J.: RASCAL: a domain specific language for source code analysis and manipulation. In: Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2009, Edmonton, Alberta, Canada, 20–21 September 2009, pp. 168–177 (2009). https://doi.org/10.1109/SCAM.2009.28
Krahn, H., Rumpe, B., Völkel, S.: MontiCore: a framework for compositional development of domain specific languages. Int. J. Softw. Tools Technol. Transf. 12(5), 353–372 (2010). https://doi.org/10.1007/s10009-010-0142-1
Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 3–10. Association for Computing Machinery, New York (2007). https://doi.org/10.1145/1190216.1190220
Miller, D., Nadathur, G.: Programming with Higher-Order Logic, 1st edn. Cambridge University Press, Cambridge (2012)
Patterson, D., Perconti, J., Dimoulas, C., Ahmed, A.: FunTAL: reasonably mixing a functional language with assembly. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, 18–23 June 2017, pp. 495–509. ACM (2017). https://doi.org/10.1145/3062341.3062347
Rosu, G., Serbanuta, T.: An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79(6), 397–434 (2010). https://doi.org/10.1016/j.jlap.2010.03.012
Scherer, G., New, M.S., Rioux, N., Ahmed, A.: Fabulous interoperability for ML and a linear language. In: Proceedings of Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, 14–20 April 2018, pp. 146–162 (2018). https://doi.org/10.1007/978-3-319-89366-2_8
Schürmann, C.: Automating the meta theory of deductive systems. Ph.D. thesis, Department of Computer Science, Carnegie Mellon University, August 2000. http://reports-archive.adm.cs.cmu.edu/anon/2000/abstracts/00-146.html. Available as Technical Report CMU-CS-00-146
Wright, A., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994). https://doi.org/10.1006/inco.1994.1093
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Cimini, M. (2022). 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. Springer, Cham. https://doi.org/10.1007/978-3-030-95561-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-95561-8_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-95560-1
Online ISBN: 978-3-030-95561-8
eBook Packages: Computer ScienceComputer Science (R0)