Email Gateway (Sep 17 2026 at 13:06): Email Gateway (Sep 17 2026 at 13:06):From: Nikolaus <nh661@cam.ac.uk>
Dear all,
We have been working on a Python backend for the Isabelle code generator, and
I believe it has reached a level of maturity that it might be useful to other
people as well:
https://github.com/pure-py/isabelle-python-codegen
We are roughly targeting a pure, functional subset of Python we termed PurePy
(https://pure-py.github.io), which is a proper subset of Python 3.12+.
Two different Python code extraction setups are provided: Python.Python uses
only a minimal set of custom code printing, while Python.Python_Setup
includes custom code printers to utilise native Python ints, lists, and
tuples.
As this is my first time working with Isabelle in this manner, I am grateful
for any feedback. I have ported the test suite from the Go backend, so a
sizeable section of the HOL library is tested. Eventually, after some more
testing, we would like to create a submission to the AFP as well.
/Nikolaus
Nikolaus Huber, PhD
Research Associate
Institute of Computing for Climate Science
Department of Computer Science and Technology
University of Cambridge
Last updated: Sep 17 2026 at 22:43 UTC