Document Open Access Logo

A Semantics of 𝕂 into Dedukti

Authors Amélie Ledein , Valentin Blot, Catherine Dubois

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2022.12.pdf
  • Filesize: 1.03 MB
  • 22 pages

Document Identifiers

Author Details

Amélie Ledein
  • Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, France
Valentin Blot
  • Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, France
Catherine Dubois
  • ENSIIE, Samovar, Évry-Courcouronnes, France

Funding

  • Ledein, Amélie: Digicosme and EuroProofNet

Acknowledgements

We want to thank the 𝕂 team, especially Andrei Arusoaie, Xiaohong Chen, Denisa Diaconescu, Everett Hildenbrandt, Zhengyao Lin, Dorel Lucanu, Ana Pantilie and Traian-Florin Serbanuta for their prompt responses to our many questions.

Cite AsGet BibTex

Amélie Ledein, Valentin Blot, and Catherine Dubois. A Semantics of 𝕂 into Dedukti. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.12

Abstract

𝕂 is a semantical framework for formally describing the semantics of programming languages thanks to a BNF grammar and rewriting rules on configurations. It is also an environment that offers various tools to help programming with the languages specified in the formalism. For example, it is possible to execute programs thanks to the generated interpreter, or to check their properties thanks to the provided automatic theorem prover called the KProver. 𝕂 is based on la Matching Logic, a first-order logic with an application and fixed-point operators, extended with symbols to encode equality, typing and rewriting. This specific la Matching Logic theory is called Kore. Dedukti is a logical framework having for main goal the interoperability of proofs between different formal proof tools. Several translators to Dedukti exist or are under development, in order to automatically translate formalizations written, for instance, in Coq or PVS. Dedukti is based on the λΠ-calculus modulo theory, a λ-calculus with dependent types and extended with a primitive notion of computation defined by rewriting rules. The flexibility of this logical framework allows to encode many theories ranging from first-order logic to the Calculus of Constructions. In this article, we present a paper formalization of the translation from 𝕂 into Kore, and a paper formalization and an automatic translation tool, called KaMeLo, from Kore to Dedukti in order to execute programs in Dedukti.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
Keywords
  • Programming language
  • Semantics
  • Rewriting
  • Logical framework
  • Type theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. GitLab of KaMeLo. URL: https://gitlab.com/semantiko/kamelo.
  2. Website of 𝕂. URL: https://kframework.org/.
  3. Website of Sail. URL: https://www.cl.cam.ac.uk/~pes20/sail/.
  4. Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. In TYPES: Types for Proofs and Programs, Novi SAd, Serbia, May 2016. URL: https://hal-mines-paristech.archives-ouvertes.fr/hal-01441751.
  5. Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some axioms for mathematics. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 20:1-20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.20.
  6. Denis Bogdănaş and Grigore Roşu. K-Java: A Complete Semantics of Java. In Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL'15), pages 445-456. ACM, January 2015. URL: https://doi.org/10.1145/2676726.2676982.
  7. Patrick Borras, Dominique Clément, Th. Despeyroux, Janet Incerpi, Gilles Kahn, Bernard Lang, and V. Pascual. CENTAUR: The System. In Peter B. Henderson, editor, Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, Boston, Massachusetts, USA, November 28-30, 1988, pages 14-24. ACM, 1988. URL: https://doi.org/10.1145/64135.65005.
  8. Raphaël Cauderlier and Catherine Dubois. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. In ICTAC 2016 - 13th International Colloquium on Theoretical Aspects of Computing, volume 9965 of LNCS, pages 459-468, Taipei, Taiwan, October 2016. URL: https://doi.org/10.1007/978-3-319-46750-4_26.
  9. Raphaël Cauderlier and Catherine Dubois. FoCaLiZe and Dedukti to the rescue for proof interoperability. In Mauricio Ayala-Rincón and César A. Muñoz, editors, ITP 2017: International Conference on Interactive Theorem Proving, page 532, Brasília, Brazil, September 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_9.
  10. D. Cousineau and Gilles Dowek. Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In TLCA, 2007. Google Scholar
  11. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 243-320, 1990. Google Scholar
  12. Gilles Dowek. Interacting Safely with an Unsafe Environment. CoRR, abs/2107.07662, 2021. https://arxiv.org/abs/2107.07662, URL: https://doi.org/10.4204/EPTCS.337.3.
  13. Chris Hathhorn, Chucky Ellison, and Grigore Roşu. Defining the Undefinedness of C. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), pages 336-345. ACM, June 2015. URL: https://doi.org/10.1145/2813885.2737979.
  14. Liyi Li and Elsa L. Gunter. IsaK: A Complete Semantics of 𝕂. Technical report, University of Illinois at Urbana-Champaign, June 2018. URL: https://hdl.handle.net/2142/100116.
  15. Liyi Li and Elsa L. Gunter. IsaK-static: A complete static semantics of 𝕂. In Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings, pages 196-215. Springer-Verlag Berlin Heidelberg, 2018. URL: https://doi.org/10.1007/978-3-030-02146-7_10.
  16. Liyi Li and Elsa L. Gunter. A Complete Semantics of 𝕂 and Its Translation to Isabelle. In Antonio Cerone and Peter Csaba Ölveczky, editors, Theoretical Aspects of Computing - ICTAC 2021, pages 152-171, Cham, 2021. Springer International Publishing. Google Scholar
  17. Dominic Mulligan, Scott Owens, Kathryn Gray, Tom Ridge, and Peter Sewell. Lem: Reusable Engineering of Real-world Semantics. ACM SIGPLAN Notices, 49, August 2014. URL: https://doi.org/10.1145/2628136.2628143.
  18. Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KJS: A Complete Formal Semantics of JavaScript. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), pages 346-356. ACM, June 2015. URL: https://doi.org/10.1145/2737924.2737991.
  19. Grigore Roșu and Traian Florin Șerbănută. An overview of the 𝕂 semantic framework. The Journal of Logic and Algebraic Programming, 79(6):397-434, August 2010. URL: https://doi.org/10.1016/j.jlap.2010.03.012.
  20. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnis̆a. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20(1):71-122, 2010. URL: https://doi.org/10.1017/S0956796809990293.
  21. Andrei Stefănescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Roşu. Semantics-based program verifiers for all languages. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 74-91, Amsterdam Netherlands, October 2016. ACM. URL: https://doi.org/10.1145/2983990.2984027.
  22. François Thiré. Sharing a library between proof assistants: Reaching out to the HOL family. Electronic Proceedings in Theoretical Computer Science, 274:57-71, July 2018. URL: https://doi.org/10.4204/eptcs.274.5.
  23. M. G. J. van den Brand, A. van Deursen, J. Heering, H. A. de Jong, M. de Jonge, T. Kuipers, P. Klint, L. Moonen, P. A. Olivier, J. Scheerder, J. J. Vinju, E. Visser, and J. Visser. The Asf+Sdf Meta-environment: A Component-Based Language Development Environment. In Reinhard Wilhelm, editor, Compiler Construction, pages 365-370, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-45306-7_26.
  24. Patrick Viry. Elimination of Conditions. Journal of Symbolic Computation, 28(3):381-401, 1999. URL: https://doi.org/10.1006/jsco.1999.0288.
  25. Glynn Winskel. The formal semantics of programming languages - an introduction. Foundation of computing series. MIT Press, 1993. Google Scholar
  26. A.K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, November 1994. URL: https://doi.org/10.1006/inco.1994.1093.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact