The Design, Evolution, and Use of KernelF

An Extensible and Embeddable Functional Language
  • Markus Voelter
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10888)


KernelF is a functional language built on top of MPS. It is designed to be highly extensible and embeddable in order to support its use at the core of domain-specific languages, realising an approach we sometimes call Funclerative Programming. “Funclerative” is of course a mash-up of “functional” and “declarative” and refers to the idea of using functional programming in the small, and declarative language constructs for the larger-scale, often domain-specific, structures in a program. We have used KernelF in a wide range of languages including health and medicine, insurance contract definition, security analysis, salary calculations, smart contracts and language-definition. In this paper, I illustrate the evolution of KernelF over the last two years. I discuss requirements on the language, and how those drove design decisions. I showcase a couple of the DSLs we built on top of KernelF to explain how MPS was used to enable the necessary language modularity. I demonstrate how we have integrated the Z3 solver to verify some aspects of programs. I present the architecture we have used to use KernelF-based DSLs in safety-critical environments. I close the keynote with an outlook on how KernelF might evolve in the future, and point out a few challenges for which we don’t yet have good solutions.


Domain-specific languages Language modularity Functional Language Language engineering Meta programming 



I implemented most of KernelF myself. However, this would not have been possible without the team at itemis: they were sparring partners in design discussions, they helped mature the language by using and stressing it, they built some of the features in the case studies, and generally provided the fertile ground on which something like KernelF can flourish. I also want to thank our customers. Not just those of the particular systems described in the case studies, but all of them: without their trust in us and, ultimately, their money, none of what is discussed in this paper would have happened. Finally, I want to thank the MPS team at Jetbrains for building an amazing tool and for helping us use it productively over the years.


  1. 1.
    Amani, S., Bégel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, 8–9 January 2018, Los Angeles, CA, USA, pp. 66–77 (2018).
  2. 2.
    Berger, T., Völter, M., Jensen, H.P., Dangprasert, T., Siegmund, J.: Efficiency of projectional editing: a controlled experiment. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 763–774. ACM (2016)Google Scholar
  3. 3.
    Booth, S.P., Jones, S.B.: Walk backwards to happiness: debugging by time travel. In: Proceedings of the 3rd International Workshop on Automatic Debugging (AADEBUG 1997), no. 001, pp. 171–184. Linköping University Electronic Press (1997)Google Scholar
  4. 4.
    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, pp. 84–89. ACM (2016)Google Scholar
  5. 5.
    Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. Commun. ACM 51(1), 107–113 (2008)CrossRefGoogle Scholar
  6. 6.
    DeRemer, F., Kron, H.H.: Programming-in-the-large versus programming-in-the-small. IEEE Trans. Softw. Eng. 2, 80–86 (1976)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Douceur, J.R.: The sybil attack. In: Druschel, P., Kaashoek, F., Rowstron, A. (eds.) IPTPS 2002. LNCS, vol. 2429, pp. 251–260. Springer, Heidelberg (2002). Scholar
  8. 8.
    Efftinge, S., Eysholdt, M., Köhnlein, J., Zarnekow, S., von Massow, R., Hasselbring, W., Hanus, M.: Xbase: implementing domain-specific languages for Java. ACM SIGPLAN Not. 48, 112–121 (2012)Google Scholar
  9. 9.
    Erdweg, S., Giarrusso, P.G., Rendel, T.: Language composition untangled. In: Proceedings of the Twelfth Workshop on Language Descriptions, Tools, and Applications, p. 7. ACM (2012)Google Scholar
  10. 10.
    Fowler, M.: Language workbenches: the killer-app for domain specific languages (2005)Google Scholar
  11. 11.
    Frantz, C.K., Nowostawski, M.: From institutions to code: towards automated generation of smart contracts. In: IEEE International Workshops on Foundations and Applications of Self* Systems, pp. 210–215. IEEE (2016)Google Scholar
  12. 12.
    Gibbons, R.: A Primer in Game Theory. Harvester Wheatsheaf, Bushey (1992)zbMATHGoogle Scholar
  13. 13.
    Hanmer, R.: Patterns for Fault Tolerant Software. Wiley, Chichester (2013)Google Scholar
  14. 14.
    Hickey, R.: The Clojure programming language. In: Proceedings of the 2008 Symposium on Dynamic Languages, p. 1. ACM (2008)Google Scholar
  15. 15.
    Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017). Scholar
  16. 16.
    Jensen, C.S., Snodgrass, R.T.: Temporal data management. IEEE Trans. Knowl. Data Eng. 11(1), 36–44 (1999)CrossRefGoogle Scholar
  17. 17.
    Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649–678 (2011)CrossRefGoogle Scholar
  18. 18.
    Korpela, K., Hallikas, J., Dahlberg, T.: Digital supply chain transformation toward blockchain integration. In: Proceedings of the 50th Hawaii International Conference on System Sciences (2017)Google Scholar
  19. 19.
    Narasimban, P., Moser, L.E., Melliar-Smith, P.M.: Using interceptors to enhance CORBA. Computer 32(7), 62–68 (1999)CrossRefGoogle Scholar
  20. 20.
    Odersky, M., Altherr, P. Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An overview of the Scala programming language. Technical report (2004)Google Scholar
  21. 21.
    Peters, G.W., Panayi, E.: Understanding modern banking ledgers through blockchain technologies: future of transaction processing and smart contracts on the internet of money. In: Tasca, P., Aste, T., Pelizzon, L., Perony, N. (eds.) Banking Beyond Banks and Money, pp. 239–278. Springer, Cham (2016). Scholar
  22. 22.
    Tapscott, D., Tapscott, A.: Blockchain Revolution: How the Technology Behind Bitcoin is Changing Money, Business, and the World. Penguin, Toronto (2016)Google Scholar
  23. 23.
    Voelter, M.: A smart contract development stack. Posted 6 December 2017Google Scholar
  24. 24.
    Voelter, M.: Language and IDE modularization and composition with MPS. In: Lämmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2011. LNCS, vol. 7680, pp. 383–430. Springer, Heidelberg (2013). Scholar
  25. 25.
    Voelter, M.: The kernelF reference (2018)Google Scholar
  26. 26.
    Voelter, M.: Language development with MPS - a quick overview (2018)Google Scholar
  27. 27.
    Voelter, M., vand Deursen, A., Kolb, B., Eberle, S.: Using C language extensions for developing embedded software: a case study. In: Proceedings of OOPSLA 2015, pp. 655–674. ACM (2015)CrossRefGoogle Scholar
  28. 28.
    Voelter, M., Kolb, B., Szabó, T., Ratiu, D., van Deursen, A.: Lessons learned from developing mbeddr: a case study in language engineering with MPS. Softw. Syst. Model. (2017).
  29. 29.
    Voelter, M., Lisson, S.: Supporting diverse notations in MPS’ projectional editor. In: GEMOC Workshop (2014)Google Scholar
  30. 30.
    Voelter, M., Ratiu, D., Kolb, B., Schaetz, B.: mbeddr: instantiating a language workbench in the embedded software domain. Autom. Softw. Eng. 20(3), 1–52 (2013)CrossRefGoogle Scholar
  31. 31.
    Voelter, M. Szabó, T., Lisson, S., Kolb, B., Erdweg, S., Berger, T.: Efficient development of consistent projectional editors using grammar cells. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language Engineering, pp. 28–40. ACM (2016)Google Scholar
  32. 32.
    Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Pap. 151, 1–32 (2014)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Markus Voelter
    • 1
  1. 1.StuttgartGermany

Personalised recommendations