Skip to main content
Springer Nature Link
Log in

A Complete Semantics of \(\mathbb {K}\) and Its Translation to Isabelle

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2021 (ICTAC 2021)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12819))

Included in the following conference series:

  • 641 Accesses

Abstract

\(\mathbb {K}\) [46] is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. Isabelle/HOL [41] is a generic proof engine which allows mathematical formulas to be built into a formal language and provides tools to prove those formulas in a logical calculus. In this paper we define IsaK, a reference semantics for \(\mathbb {K}\), which was developed through discussions with the \(\mathbb {K}\) team to meet their expectations for a semantics for \(\mathbb {K}\). Previously, we defined the static semantics for \(\mathbb {K}\) [28]; thus, this paper mainly focuses on its dynamic semantics. More importantly, we investigate a way to connect \(\mathbb {K}\) and Isabelle by building a translation framework, TransK, to translate programming languages defined in \(\mathbb {K}\) into theories defined in Isabelle, which can not only allow programmers to define their programming languages easily in \(\mathbb {K}\) but also have the ability to reason about their languages in Isabelle. In order to show a well-established translation, we prove that the \(\mathbb {K}\) specification is sound and relatively complete with respect to the translated Isabelle theory by TransK. To the best of our knowledge, IsaK is the first complete formal semantics defined for \(\mathbb {K}\), while TransK is the first complete translation from a real-world, order-sorted algebraic system to a many-sorted one. All the work is formalized in Isabelle/HOL at https://github.com/liyili2/KtoIsabelle.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
€32.70 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 64.19
Price includes VAT (France)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 79.11
Price includes VAT (France)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. 235, 98–136 (2014)

    Article  MathSciNet  Google Scholar 

  2. Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_1http://dl.acm.org/citation.cfm?id=1987211.1987212

    Chapter  Google Scholar 

  3. Beierle, C., Meyer, G.: Run-time type computations in the Warren Abstract Machine. J. Log. Program. 18(2), 123–148 (1994)

    Article  MathSciNet  Google Scholar 

  4. Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263–288 (2009)

    Article  MathSciNet  Google Scholar 

  5. Bogdănaş, D., Roşu, G.: K-Java: a complete semantics of Java. In: Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL 2015), pp. 445–456. ACM, January 2015

    Google Scholar 

  6. Comon, H.: Equational formulas in order-sorted algebras. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 674–688. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0032066

    Chapter  Google Scholar 

  7. Corbineau, P.: A declarative language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 69–84. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68103-8_5

    Chapter  MATH  Google Scholar 

  8. Şerbănuţă, T.F., Roşu, G.: K-Maude: a rewriting based tool for semantics of programming languages. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 104–122. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16310-4_8

    Chapter  MATH  Google Scholar 

  9. Ştefănescu, A., Ciobâcă, Ş, Mereuta, R., Moore, B.M., Şerbănută, T.F., Roşu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 425–440. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08918-8_29

    Chapter  Google Scholar 

  10. Ştefănescu, A., Park, D., Yuwen, S., Li, Y., Roşu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 31th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016), pp. 74–91. ACM, November 2016

    Google Scholar 

  11. Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Talcott, C.: Pathway logic: executable models of biological networks. In: Fourth International Workshop on Rewriting Logic and Its Applications (WRLA 2002). Electronic Notes in Theoretical Computer Science, Pisa, Italy, 19–21 September 2002, vol. 71. Elsevier (2002). http://www.elsevier.nl/locate/entcs/volume71.html

  12. Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 230–234. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44829-2_16http://dl.acm.org/citation.cfm?id=1767111.1767127

    Chapter  MATH  Google Scholar 

  13. Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pp. 533–544. ACM, January 2012

    Google Scholar 

  14. Filaretti, D., Maffeis, S.: An executable formal semantics of PHP. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 567–592. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44202-9_23

    Chapter  Google Scholar 

  15. Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Operational semantics for order-sorted algebra. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 221–231. Springer, Heidelberg (1985). https://doi.org/10.1007/BFb0015747http://dl.acm.org/citation.cfm?id=646239.683375

    Chapter  Google Scholar 

  16. Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217–273 (1992)

    Article  MathSciNet  Google Scholar 

  17. Hathhorn, C., Ellison, C., Roşu, G.: Defining the undefinedness of C. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pp. 336–345. ACM, June 2015

    Google Scholar 

  18. Hills, M., Roşu, G.: Towards a module system for K. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 187–205. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03429-9_13

    Chapter  Google Scholar 

  19. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

  20. Hullot, J.M.: Associative commutative pattern matching. In: Proceedings of the 6th International Joint Conference on Artificial Intelligence, IJCAI 1979, vol. 1, pp. 406–412. Morgan Kaufmann Publishers Inc., San Francisco (1979)

    Google Scholar 

  21. Inwegen, M.V., Gunter, E.L.: HOL-ML. In: Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993, Vancouver, BC, Canada, 11–13 August 1993, pp. 61–74 (1993)

    Google Scholar 

  22. Kirchner, C., Kirchner, H., Meseguer, J.: Operational semantics of OBJ-3. In: Lepistö, T., Salomaa, A. (eds.) ICALP 1988. LNCS, vol. 317, pp. 287–301. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-19488-6_123

    Chapter  Google Scholar 

  23. Krebber, M.: Non-linear associative-commutative many-to-one pattern matching with sequence variables. ArXiv abs/1705.00907 (2017)

    Google Scholar 

  24. Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. SIGPLAN Not. 42(1), 173–184 (2007)

    Article  Google Scholar 

  25. Li, L., Gunter, E.: A method to translate order-sorted algebras to many-sorted algebras. In: Proceedings of the Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2017. EPTCS (2017)

    Google Scholar 

  26. Li, L., Gunter, E.: K-LLVM: a relatively complete semantics of LLVM IR. In: Donaldson, A.F. (ed.) 34rd European Conference on Object-Oriented Programming, ECOOP 2020. LIPIcs, Berlin, Germany, 13–17 July 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

    Google Scholar 

  27. Li, L., Gunter, E.: Tech Report for a Complete Semantics of K and Its Translation to Isabelle (2021). https://github.com/liyili2/KtoIsabelle/blob/master/tech-report.pdf

  28. Li, L., Gunter, E.L.: IsaK-Static: a complete static semantics of \(\mathbb{K}\). In: Bae, K., Ölveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 196–215. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02146-7_10

    Chapter  Google Scholar 

  29. Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of maude. In: Meseguer, J. (ed.) Electronic Notes in Theoretical Computer Science, vol. 4. Elsevier Science Publishers (2000)

    Google Scholar 

  30. Maharaj, S., Gunter, E.: Studying the ML module system in HOL. In: Melham, T.F., Camilleri, J. (eds.) HUG 1994. LNCS, vol. 859, pp. 346–361. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58450-1_53

    Chapter  Google Scholar 

  31. Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theor. Comput. Sci. 285(2), 121–154 (2002). Rewriting Logic and Its Applications. http://www.sciencedirect.com/science/article/pii/S0304397501003577

  32. Matache, C., Gomes, V.B.F., Mulligan, D.P.: The LambdaMu-calculus. Archive of Formal Proofs 2017 (2017). https://www.isa-afp.org/entries/LambdaMu.html

  33. Meseguer, J.: Research directions in rewriting logic. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic. NATO ASI Series, vol. 165, pp. 347–398. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-642-58622-4_10

    Chapter  MATH  Google Scholar 

  34. Meseguer, J.: Software specification and verification in rewriting logic. In: Nato Science Series Sub Series III Computer and Systems Sciences, vol. 191, pp. 133–194 (2003)

    Google Scholar 

  35. Meseguer, J., Goguen, J.A., Smolka, G.: Order-sorted unification. J. Symb. Comput. 8(4), 383–413 (1989)

    Article  MathSciNet  Google Scholar 

  36. Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Formal Aspects Comput. 29(3), 423–452 (2017). https://doi.org/10.1007/s00165-017-0415-5

    Article  MathSciNet  MATH  Google Scholar 

  37. Milner, R., Tofte, M., Macqueen, D.: The Definition of Standard ML. MIT Press, Cambridge (1997)

    Book  Google Scholar 

  38. Moore, B., Roşu, G.: Program verification by coinduction. Technical report, University of Illinois, February 2015. http://hdl.handle.net/2142/73177

  39. Norrish, M.: C formalised in HOL. Technical report, Computer Laboratory, University of Cambridge (1998)

    Google Scholar 

  40. Park, D., Ştefănescu, A., Roşu, G.: KJS: a complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pp. 346–356. ACM, June 2015

    Google Scholar 

  41. Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press (1990)

    Google Scholar 

  42. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74, July 2002

    Google Scholar 

  43. Roşu, G.: K: a rewriting-based framework for computations - preliminary version. Technical report, Department of Computer Science UIUCDCS-R-2007-2926 and College of Engineering UILU-ENG-2007-1827, University of Illinois at Urbana-Champaign (2007). Previous versions published as technical reports UIUCDCS-R-2006-2802 in December 2006, UIUCDCS-R-2005-2672 in 2005. K was first introduced in the context of Maude in Fall 2003 as part of a programming language design course (technical report UIUCDCS-R-2003-2897)

    Google Scholar 

  44. Roşu, G.: K Publications (2017). http://www.kframework.org/index.php/K_Publications

  45. Roşu, G., Ştefănescu, A., Ciobâcă, C., Moore, B.M.: One-path reachability logic. In: Proceedings of the 28th Symposium on Logic in Computer Science (LICS 2013), pp. 358–367. IEEE, June 2013

    Google Scholar 

  46. Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Log. Algebraic Program. 79(6), 397–434 (2010)

    Article  MathSciNet  Google Scholar 

  47. Roşu, G., Ştefănescu, A.: Matching logic: a new program verification approach. In: Proceedings of the 2010 Workshop on Usable Verification (UV 2010). Microsoft Research (2010)

    Google Scholar 

  48. Wang, H.: Logic of many-sorted theories. J. Symb. Log. 17(2), 105–116 (1952). https://doi.org/10.2307/2266241

    Article  MathSciNet  MATH  Google Scholar 

  49. Şerbănuţă, T.F., Arusoaie, A., Lazar, D., Ellison, C., Lucanu, D., Roşu, G.: The K primer (version 3.3). Electron. Notes Theor. Comput. Sci. 304(Supplement C), 57–80 (2014). Proceedings of the Second International Workshop on the K Framework and Its Applications (K 2011). http://www.sciencedirect.com/science/article/pii/S1571066114000395

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Maryland, College Park, USA

    Liyi Li

  2. Department of Computer Science, University of Illinois at Urbana-Champaign, Champaign, USA

    Elsa L. Gunter

Authors
  1. Liyi Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Elsa L. Gunter
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Liyi Li .

Editor information

Editors and Affiliations

  1. Nazarbayev University, Nur-Sultan, Kazakhstan

    Antonio Cerone

  2. Department of Informatics, University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Li, L., Gunter, E.L. (2021). A Complete Semantics of \(\mathbb {K}\) and Its Translation to Isabelle. In: Cerone, A., Ölveczky, P.C. (eds) Theoretical Aspects of Computing – ICTAC 2021. ICTAC 2021. Lecture Notes in Computer Science(), vol 12819. Springer, Cham. https://doi.org/10.1007/978-3-030-85315-0_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-85315-0_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-85314-3

  • Online ISBN: 978-3-030-85315-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation