Type Theory as a Framework for Modelling and Programming

  • Cezar Ionescu
  • Patrik JanssonEmail author
  • Nicola Botta
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11244)


In the context provided by the proceedings of the UVMP track of ISoLA 2016, we propose Type Theory as a suitable framework for both modelling and programming. We show that it fits most of the requirements put forward on such frameworks by Broy et al. and discuss some of the objections that can be raised against it.


Software technology Specification Functional programming Dependent types Domain-specific languages 



The work presented in this paper heavily relies on free software, among others on Idris, Agda, GHC, git, vi, Emacs, Open image in new window and on the FreeBSD and Debian GNU/Linux operating systems. It is our pleasure to thank all developers of these excellent products. This work was partially supported by the CoeGSS project (grant agreement No. 676547), which has received funding from the European Union’s Horizon 2020 research and innovation programme.


  1. 1.
    Altenkirch, T.: Naive type theory (2017). Lecture Notes for a course at MGS 2017
  2. 2.
    Bar, K., Kissinger, A., Vicary, J.: Globular: an online proof assistant for higher-dimensional rewriting. Logical Methods Comput. Sci. 14(1) (2018).
  3. 3.
    Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, S.E. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 117–309. Oxford University Press Inc., New York (1992).
  4. 4.
    Berry, G.: Formally unifying modeling and design for embedded systems - a personal view. In: Margaria and Steffen [38], pp. 134–149. Scholar
  5. 5.
    Bishop, E., Bridges, D.: Constructive Analysis. Springer, Heidelberg (1985). Scholar
  6. 6.
    Botta, N., Jansson, P., Ionescu, C.: Contributions to a computational theory of policy advice and avoidability. J. Funct. Program. 27, 1–52 (2017). Scholar
  7. 7.
    Bourbaki, N.: Éléments de mathématique: Fasc. I. Livre 1, Théorie des ensembles; [5], Fascicule de résultats. Hermann (1964)Google Scholar
  8. 8.
    Bourbaki, N.: Théorie des ensembles. Springer, Heidelberg (2006). Scholar
  9. 9.
    Brady, E.: The IDRIS programming language – implementing embedded domain specific languages with dependent types. In: Central European Functional Programming School - 5th Summer School, CEFP 2013, Cluj-Napoca, Romania, 8 July–20 2013, Revised Selected Papers, pp. 115–186 (2013). Scholar
  10. 10.
    Brady, E.: Type-driven development of concurrent communicating systems. Comput. Sci. 18(3) (2017). Scholar
  11. 11.
    Brady, E., Hammond, K.: Resource-safe systems programming with embedded domain specific languages. In: Russo, C., Zhou, N.F. (eds.) PADL 2012. LNCS, vol. 7149, pp. 242–257. Springer, Heidelberg (2012). Scholar
  12. 12.
    Broy, M., Havelund, K., Kumar, R.: Towards a unified view of modeling and programming. In: Margaria and Steffen [38], pp. 238–257. Scholar
  13. 13.
    Chlipala, A.: Ur: Statically-typed metaprogramming with type-level record computation. In: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, pp. 122–133. ACM, New York (2010).
  14. 14.
    Coecke, B., Kissinger, A.: Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, Cambridge (2017)CrossRefGoogle Scholar
  15. 15.
    Elaasar, M., Badreddin, O.: Modeling meets programming: a comparative study in model driven engineering action languages. In: Margaria and Steffen [38], pp. 50–67. Scholar
  16. 16.
    Elmqvist, H., Henningsson, T., Otter, M.: Systems modeling and programming in a unified environment based on Julia. In: Margaria and Steffen [38], pp. 198–217. Scholar
  17. 17.
    ForMath project team: Papers and slides from the “formalisation of mathematics” (ForMath) project.
  18. 18.
    Fritzson, P.: Principles of Object-oriented Modeling and Simulation with Modelica 2.1. Wiley, Hoboken (2010)CrossRefGoogle Scholar
  19. 19.
    Halmos, P.: Naive Set Theory. Van Nostrand (1960). Reprinted by Springer-Verlag, Undergraduate Texts in Mathematics (1974)Google Scholar
  20. 20.
    Haxthausen, A.E., Peleska, J.: On the feasibility of a unified modelling and programming paradigm. In: Margaria and Steffen [38], pp. 32–49. Scholar
  21. 21.
    Igried, B., Setzer, A.: Programming with monadic CSP-style processes in dependent type theory. In: Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016, pp. 28–38. ACM, New York (2016).
  22. 22.
    Ionescu, C.: Vulnerability modelling and monadic dynamical systems. Ph.D. thesis, Freie Universität Berlin (2009)Google Scholar
  23. 23.
    Ionescu, C.: Vulnerability modelling with functional programming and dependent types. Math. Struct. Comput. Sci. 26(01), 114–128 (2016). Scholar
  24. 24.
    Ionescu, C., Jansson, P.: Domain-specific languages of mathematics: presenting mathematical analysis using functional programming. In: Proceedings of the 4th and 5th International Workshop on Trends in Functional Programming in Education, TFPIE 2016, Sophia-Antipolis, France and University of Maryland College Park, USA, 2nd June 2015 and 7th June 2016, pp. 1–15 (2016). Scholar
  25. 25.
    Jansson, P., Einarsdóttir, S.H., Ionescu, C.: Examples and results from a BSc-level course on domain specific languages of mathematics. In: Proceedings 7th International Workshop on Trends in Functional Programming in Education. EPTCS, Open Publishing Association (2018, in submission). Presented at TFPIE 2018Google Scholar
  26. 26.
    Jansson, P., Ionescu, C.: Domain specific languages of mathematics: Lecture notes (2018).
  27. 27.
    Jeffrey, A.: Dependently typed web client applications. In: Sagonas, K. (ed.) Practical Aspects of Declarative Languages (PADL), pp. 228–243. Springer, Heidelberg (2013). Scholar
  28. 28.
    Kugler, H.: Unifying modelling and programming: a systems biology perspective. In: Margaria and Steffen [38], pp. 131–133. Scholar
  29. 29.
  30. 30.
    Landin, P.J.: The next 700 programming languages. Commun. ACM 9(3), 157–166 (1966)CrossRefGoogle Scholar
  31. 31.
    Larsen, P.G., Fitzgerald, J.S., Woodcock, J., Nilsson, R., Gamble, C., Foster, S.: Towards semantically integrated models and tools for cyber-physical systems design. In: Margaria and Steffen [38], pp. 171–186. Scholar
  32. 32.
    Larsen, P.G., et al.: VDM-10 Language Manual. Technical report TR-001, The Overture Initiative, April 2013.
  33. 33.
    Lattmann, Z., Kecskés, T., Meijer, P., Karsai, G., Völgyesi, P., Lédeczi, Á.: Abstractions for modeling complex systems. In: Margaria and Steffen [38], pp. 68–79. Scholar
  34. 34.
    Leavens, G.T., Naumann, D.A., Rajan, H., Aotani, T.: Specifying and verifying advanced control features. In: Margaria and Steffen [38], pp. 80–96. Scholar
  35. 35.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). Scholar
  36. 36.
    Lethbridge, T.C., Abdelzad, V., Orabi, M.H., Orabi, A.H., Adesina, O.: Merging modeling and programming using Umple. In: Margaria and Steffen [38], pp. 187–197. Scholar
  37. 37.
    Ludewig, J.: Models in software engineering - an introduction. Softw. Syst. Model 2, 5–14 (2003). Scholar
  38. 38.
    Margaria, T., Steffen, B. (eds.): ISoLA 2016. LNCS, vol. 9953. Springer, Cham (2016). Scholar
  39. 39.
    Marlow, S.: Parallel and concurrent programming in Haskell. In: Zsók, V., Horváth, Z., Plasmeijer, R. (eds)Central European Functional Programming School: 4th Summer School. LNCS, vol. 7241, pp. 339–401. Springer, Heidelberg (2012). Scholar
  40. 40.
    MBE Visual Glossary project: Model-based engineering visual glossary (2017).
  41. 41.
    Morgenstern, J., Licata, D.: Security-typed programming within dependently-typed programming. In: International Conference on Functional Programming. ACM (2010).
  42. 42.
    Naujokat, S., Neubauer, J., Margaria, T., Steffen, B.: Meta-level reuse for mastering domain specialization. In: Margaria and Steffen [38], pp. 218–237. Scholar
  43. 43.
    Object Management Group (OMG): Unified modeling language. OMG Document Number formal/17-12-05 (2017).
  44. 44.
    Oury, N., Swierstra, W.: The power of Pi. In: Proceedings of ICFP 2008, pp. 39–50. ACM (2008).
  45. 45.
    Pierce, B.C.: Types and Programming Languages, 1st edn. MIT Press, Cambridge (2002)zbMATHGoogle Scholar
  46. 46.
    Prinz, A., Møller-Pedersen, B., Fischer, J.: Modelling and testing of real systems. In: Margaria and Steffen [38], pp. 119–130. Scholar
  47. 47.
    Protzenko, J., et al.: Verified low-level programming embedded in F*. In: Proceedings of the ACM on Programming Languages 1(ICFP), pp. 17:1–17:29, August 2017. Scholar
  48. 48.
    Rouquette, N.F.: Simplifying OMG MOF-based metamodeling. In: Margaria and Steffen [38], pp. 97–118. Scholar
  49. 49.
    Rybicki, F., Smyth, S., Motika, C., Schulz-Rosengarten, A., von Hanxleden, R.: Interactive model-based compilation continued - incremental hardware synthesis for SCCharts. In: Margaria and Steffen [38], pp. 150–170. Scholar
  50. 50.
    Seidewitz, E.: On a unified view of modeling and programming position paper. In: Margaria and Steffen [38], pp. 27–31. Scholar
  51. 51.
    Selic, B.: Programming \(\subset \) modeling \(\subset \) engineering. In: Margaria and Steffen [38], pp. 11–26. Scholar
  52. 52.
    Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. Proc. ICFP 2011, 266–278 (2011). Scholar
  53. 53.
    Turner, R.: Computable Models. Springer, Heidelberg (2009). Scholar
  54. 54.
    Wells, C.: Communicating mathematics: useful ideas from computer science. Am. Math. Monthl., 397–408 (1995). Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of OxfordOxfordUK
  2. 2.Chalmers University of TechnologyGothenburgSweden
  3. 3.Potsdam Institute for Climate Impact ResearchPotsdamGermany

Personalised recommendations