Document Open Access Logo

Contextual MetaML: Syntax and Full Abstraction

Authors Haoxuan Yin , Andrzej S. Murawski , C.-H. Luke Ong

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.83.pdf
  • Filesize: 0.86 MB
  • 27 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
  • Software and its engineering → Imperative languages
  • Theory of computation → Type theory
Keywords
  • Metaprogramming
  • operational game semantics
  • trace model
  • contextual modal type theory

Metrics

Abstract

MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual MetaML, the first metaprogramming language that supports storing and running open code under a strong type safety guarantee. The type system utilises contextual modal types to track and reason about free variables in code explicitly.
A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing the first full abstraction result for an imperative MetaML-style language. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.

Cite As Get BibTex

Haoxuan Yin, Andrzej S. Murawski, and C.-H. Luke Ong. Contextual MetaML: Syntax and Full Abstraction. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 83:1-83:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.83

Author Details

Haoxuan Yin
  • University of Oxford, UK
Andrzej S. Murawski
  • University of Oxford, UK
C.-H. Luke Ong
  • Nanyang Technological University, Singapore

Funding

The work was partially supported by National Research Foundation, Singapore, under its RSS Scheme (NRF-RSS2022-009).
  • Yin, Haoxuan: funded by Oxford-DeepMind Graduate Scholarship.

Acknowledgements

We thank the reviewers for their helpful comments.

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full Abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. URL: https://doi.org/10.1006/INCO.2000.2930.
  2. Samson Abramsky and C.-H. Luke Ong. Full Abstraction in the Lazy Lambda Calculus. Inf. Comput., 105(2):159-267, 1993. URL: https://doi.org/10.1006/INCO.1993.1044.
  3. Martin Berger and Laurence Tratt. Program Logics for Homogeneous Generative Run-Time Meta-Programming. Log. Methods Comput. Sci., 11(1), 2015. URL: https://doi.org/10.2168/LMCS-11(1:5)2015.
  4. Martin Berger, Laurence Tratt, and Christian Urban. Modelling Homogeneous Generative Meta-Programming. In Peter Müller, editor, 31st European Conference on Object-Oriented Programming, volume 74 of LIPIcs, pages 5:1-5:23, 2017. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.5.
  5. Peio Borthelle, Guilhem Jaber, Tom Hirschowitz, and Yannick Zakowski. An abstract, certified account of operational game semantics. In ESOP'25, Hamilton, Canada, 2025. Google Scholar
  6. Cristiano Calcagno, Eugenio Moggi, and Tim Sheard. Closed types for a safe imperative MetaML. Journal of Functional Programming, 13(3):545-571, 2003. URL: https://doi.org/10.1017/S0956796802004598.
  7. Tsung-Ju Chiang, Jeremy Yallop, Leo White, and Ningning Xie. Staged Compilation with Module Functors. Proc. ACM Program. Lang., 8(ICFP):693-727, 2024. URL: https://doi.org/10.1145/3674649.
  8. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program., 22(4-5):477-528, 2012. URL: https://doi.org/10.1017/S095679681200024X.
  9. Andrew D. Gordon. Bisimilarity as a Theory of Functional Programming. Theor. Comput. Sci., 228(1-2):5-47, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00353-3.
  10. Furio Honsell, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott. A Variable Typed Logic of Effects. Inf. Comput., 119(1):55-90, 1995. URL: https://doi.org/10.1006/INCO.1995.1077.
  11. Jason Z. S. Hu and Brigitte Pientka. A Layered Approach to Intensional Analysis in Type Theory. ACM Trans. Program. Lang. Syst., 46(4):15:1-15:43, 2024. URL: https://doi.org/10.1145/3707203.
  12. Jason Z. S. Hu and Brigitte Pientka. Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis. In Stephanie Weirich, editor, Programming Languages and Systems, volume 14576, pages 52-82. Springer Nature Switzerland, Cham, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_3.
  13. Jason Z. S. Hu and Brigitte Pientka. A Dependent Type Theory for Meta-programming with Intensional Analysis. Proc. ACM Program. Lang., 9(POPL):15:416-15:445, 2025. URL: https://doi.org/10.1145/3704851.
  14. J. M. E. Hyland and C.-H. Luke Ong. On Full Abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285-408, 2000. URL: https://doi.org/10.1006/INCO.2000.2917.
  15. Jun Inoue and Walid Taha. Reasoning about multi-stage programs. Journal of Functional Programming, 26:e22, 2016. URL: https://doi.org/10.1017/S0956796816000253.
  16. Kanaru Isoda, Ayato Yokoyama, and Yukiyoshi Kameyama. Type-Safe Code Generation with Algebraic Effects and Handlers. In Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE '24, pages 53-65, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3689484.3690731.
  17. Guilhem Jaber and Andrzej S. Murawski. Complete trace models of state and control. In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 348-374. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_13.
  18. Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka. Møebius: Metaprogramming using contextual types: The stage where system f can pattern match on itself. Proc. ACM Program. Lang., 6(POPL):1-27, 2022. URL: https://doi.org/10.1145/3498700.
  19. Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan. Shifting the stage - Staging with delimited control. J. Funct. Program., 21(6):617-662, 2011. URL: https://doi.org/10.1017/S0956796811000256.
  20. Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan. Combinators for impure yet hygienic code generation. Sci. Comput. Program., 112:120-144, 2015. URL: https://doi.org/10.1016/J.SCICO.2015.08.007.
  21. Oleg Kiselyov. The Design and Implementation of BER MetaOCaml: System Description. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Alfred Kobsa, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Demetri Terzopoulos, Doug Tygar, Gerhard Weikum, Michael Codish, and Eijiro Sumii, editors, Functional and Logic Programming, volume 8475, pages 86-102. Springer International Publishing, Cham, 2014. URL: https://doi.org/10.1007/978-3-319-07151-0_6.
  22. Oleg Kiselyov. MetaOCaml Theory and Implementation. CoRR, abs/2309.08207, 2023. URL: https://doi.org/10.48550/arXiv.2309.08207.
  23. Oleg Kiselyov. MetaOCaml: Ten Years Later - System Description. In Jeremy Gibbons and Dale Miller, editors, Functional and Logic Programming - 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15-17, 2024, Proceedings, volume 14659 of Lecture Notes in Computer Science, pages 219-236. Springer, 2024. URL: https://doi.org/10.1007/978-981-97-2300-3_12.
  24. Oleg Kiselyov, Yukiyoshi Kameyama, and Yuto Sudo. Refined environment classifiers: Type- and scope-safe code generation with mutable cells. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings, pages 271-291. Springer Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_15.
  25. James Laird. A Fully Abstract Trace Semantics for General References. In Lars Arge, Christian Cachin, Tomasz Jurdziński, and Andrzej Tarlecki, editors, Automata, Languages and Programming, volume 4596, pages 667-679. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-73420-8_58.
  26. Soren B. Lassen and Paul Blain Levy. Typed Normal Form Bisimulation. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, pages 283-297, Berlin, Heidelberg, 2007. Springer. URL: https://doi.org/10.1007/978-3-540-74915-8_23.
  27. Paul Blain Levy and Sam Staton. Transition systems over games. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 64:1-64:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603150.
  28. Robin Milner. Fully Abstract Models of Typed λ-Calculi. Theor. Comput. Sci., 4(1):1-22, 1977. URL: https://doi.org/10.1016/0304-3975(77)90053-6.
  29. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Trans. Comput. Log., 9(3):23:1-23:49, 2008. URL: https://doi.org/10.1145/1352582.1352591.
  30. Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 371-382. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328483.
  31. Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, and Rébecca Zucchini. A Type Theory for Defining Logics and Proofs. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785683.
  32. Jurriaan Rot, Bart Jacobs, and Paul Blain Levy. Steps and traces. J. Log. Comput., 31(6):1482-1525, 2021. URL: https://doi.org/10.1093/LOGCOM/EXAB050.
  33. Tim Sheard and Simon Peyton Jones. Template meta-programming for Haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, pages 1-16, Pittsburgh Pennsylvania, October 2002. ACM. URL: https://doi.org/10.1145/581690.581691.
  34. Bjarne Stroustrup. The C++ Programming Language. Pearson Education, 2013. Google Scholar
  35. Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1999. Google Scholar
  36. Walid Taha and Tim Sheard. MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1):211-242, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00053-0.
  37. Carolyn Talcott. Reasoning about Programs With Effects. Electronic Notes in Theoretical Computer Science, 14:301-314, 1997. URL: https://doi.org/10.1016/S1571-0661(05)80243-9.
  38. David Vandevoorde, Nicolai M. Josuttis, and Douglas Gregor. C++ Templates: The Complete Guide (2nd Edition). Addison-Wesley Professional, 2nd edition, 2017. Google Scholar
  39. Edwin Westbrook, Mathias Ricken, Jun Inoue, Yilong Yao, Tamer Abdelatif, and Walid Taha. Mint: Java multi-stage programming using weak separability. ACM SIGPLAN Notices, 45(6):400-411, 2010. URL: https://doi.org/10.1145/1809028.1806642.
  40. Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang. Staging with class: A specification for typed template Haskell. Proceedings of the ACM on Programming Languages, 6(POPL):61:1-61:30, January 2022. URL: https://doi.org/10.1145/3498723.
  41. Ningning Xie, Leo White, Olivier Nicole, and Jeremy Yallop. MacoCaml: Staging Composable and Compilable Macros. Proceedings of the ACM on Programming Languages, 7(ICFP):209:604-209:648, 2023. URL: https://doi.org/10.1145/3607851.
  42. Haoxuan Yin, Andrzej S. Murawski, and C. H. Luke Ong. Layered modal ML: Syntax and full abstraction, 2026. URL: https://doi.org/10.48550/arXiv.2602.03033.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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