Document Open Access Logo

A Rational Defense of Reasonable Reflection (Invited Paper)

Author Nada Amin

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.1.pdf
  • Filesize: 0.68 MB
  • 5 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • reflection
  • verification
  • AI

Metrics

Abstract

Computational reflection is the ability of a system to inspect and modify itself. It has resisted static reasoning, especially in reflective languages, where semantics can change during program execution. We argue that reflection should be revisited in light of progress in verification and large language models. By requiring reflective modifications to carry proofs, it becomes possible to prove system properties even for reflective systems. This "reasonable reflection" could open up new ways of organizing self-improving systems.

Cite As Get BibTex

Nada Amin. A Rational Defense of Reasonable Reflection (Invited Paper). In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.1

Author Details

Nada Amin
  • Harvard University, Cambridge, MA, USA

Funding

Amazon Research Award and Google Cloud for compute credits.

Acknowledgements

Thanks to Kenichi Asai, Matko Bošnjak, Will Byrd, Steve Chong, Kartik Chandra, Olivier Danvy, Michael Fogus, Walter Fontana, Fernanda Graciolli, Simon Henniger, Tzu-Han Hsu, Ohad Kammar, Anastasiya Kravchuk-Kirilyuk, Paul Krogmeier, Gabriel Poesia, Christopher Qiu, Matthew Retchin, Jack Rusher, Raffi Sanna, Gerry Sussman, Eric Tanter, Mitch Wand, Cameron Wong, Haoyi Zeng, and Stefan Zetzsche for discussions.

Supplementary Materials

References

  1. Nada Amin. Reflective towers of interpreters, SIGPLAN PL Perspectives, August 2021. URL: https://blog.sigplan.org/2021/08/12/reflective-towers-of-interpreters.
  2. Nada Amin and Tiark Rompf. Collapsing towers of interpreters. Proc. ACM Program. Lang., 2(POPL), 2018. URL: https://doi.org/10.1145/3158140.
  3. Kenichi Asai. The Reflective Language Black. PhD thesis, Department of Information Science, Graduate School of Science, University of Tokyo, February 1997. Google Scholar
  4. Kenichi Asai, Satoshi Matsuoka, and Akinori Yonezawa. Duplication and partial evaluation: for a better understanding of reflective languages. Lisp Symb. Comput., 9(2–3):203-241, May 1996. URL: https://doi.org/10.1007/BF01806113.
  5. Lev D Beklemishev. Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2):197-268, 2005. Google Scholar
  6. Olivier Danvy and Karoline Malmkjær. A blond primer. Draft, DIKU, University of Copenhagen, Copenhagen, Denmark, February 1988. Google Scholar
  7. Olivier Danvy and Karoline Malmkjær. Intensions and extensions in a reflective tower. In Proceedings of the 1988 ACM Conference on LISP and Functional Programming, LFP '88, pages 327-341, New York, NY, USA, 1988. Association for Computing Machinery. URL: https://doi.org/10.1145/62678.62725.
  8. Solomon Feferman. Transfinite recursive progressions of axiomatic theories. The Journal of Symbolic Logic, 27(3):259-316, 1962. URL: https://doi.org/10.2307/2964649.
  9. Daniel P. Friedman and Mitchell Wand. Reification: Reflection without metaphysics. In Proceedings of the 1984 ACM Symposium on LISP and Functional Programming, LFP '84, pages 348-355, New York, NY, USA, 1984. Association for Computing Machinery. URL: https://doi.org/10.1145/800055.802051.
  10. Ramana Kumar. Self-compilation and self-verification. Technical Report UCAM-CL-TR-879, University of Cambridge, Computer Laboratory, February 2016. URL: https://doi.org/10.48456/tr-879.
  11. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. Proc. ACM Program. Lang., 7(OOPSLA1), 2023. URL: https://doi.org/10.1145/3586037.
  12. K Rustan M Leino. Program proofs. MIT Press, 2023. Google Scholar
  13. Douglas B Lenat. EURISKO: a program that learns new heuristics and domain concepts: the nature of heuristics III: program design and results. Artificial Intelligence, 21(1-2):61-98, 1983. Google Scholar
  14. Pattie Maes. Concepts and experiments in computational reflection. In Conference Proceedings on Object-Oriented Programming Systems, Languages and Applications, OOPSLA '87, pages 147-155, New York, NY, USA, 1987. Association for Computing Machinery. URL: https://doi.org/10.1145/38765.38821.
  15. Robin Milner. Logic for computable functions: description of a machine implementation. Technical report, Stanford University, Stanford, CA, USA, May 1972. Google Scholar
  16. Robin Milner. LCF: A way of doing proofs with a machine. In Jiří Bečvář, editor, Mathematical Foundations of Computer Science 1979, pages 146-159, Berlin, Heidelberg, 1979. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-09526-8_11.
  17. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  18. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. Google Scholar
  19. Brian Cantwell Smith. Procedural Reflection in Programming Languages. PhD thesis, Massachusetts Institute of Technology, Laboratory for Computer Science, 1982. URL: http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-272.pdf.
  20. Brian Cantwell Smith. Reflection and semantics in LISP. In Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '84, pages 23-35, New York, NY, USA, 1984. Association for Computing Machinery. URL: https://doi.org/10.1145/800017.800513.
  21. Brian Cantwell Smith. Computational Reflections. The MIT Press, May 2026. Google Scholar
  22. The Rocq Development Team. The Rocq Prover Reference Manual, version 9.2.0, 2026. URL: https://rocq-prover.org/doc/V9.2.0/refman/index.html.
  23. Mitchell Wand. The theory of fexprs is trivial. Lisp Symb. Comput., 10(3):189-199, 1998. URL: https://doi.org/10.1023/A:1007720632734.
  24. Mitchell Wand and Daniel P. Friedman. The mystery of the tower revealed: a non-reflective description of the reflective tower. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP '86, pages 298-307, New York, NY, USA, 1986. Association for Computing Machinery. URL: https://doi.org/10.1145/319838.319871.
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