Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Program Synthesis libraries or projects?

Email Gateway (Aug 07 2025 at 10:36):

From: Andrea Vezzosi <vezzosi.ndr@gmail.com>
Hello,

Are there Isabelle tools or formalizations in the area of program
synthesis?

Especially interested in ones for functional languages (e.g. (some subset
of) Haskell or ML), the end goal would be a tactic that given a
specification and a partial program (i.e. with placeholders, aka typed
holes) produces a completed program, if possible.

No particular constraints on the specification format, but the synthesis
should be flexible in the form of programs that could be synthesized,
because I would like to support a variety of partial programs as inputs.

Best regards,
Andrea

Email Gateway (Aug 07 2025 at 11:45):

From: Lawrence Paulson <lp15@cam.ac.uk>
I am not aware of any. I played around with this sort of thing 40 years ago, in the context of Martin-Löf type theory. It was supposedly one of the main benefits of MLTT (as people argued at the time), but I found it really difficult.

A bit later, a student of mine (Martin Coen) did some experiments and built what he called Classical Computational Logic for Untyped Lambda Calculus, which is still available in the distribution as Isabelle/CCL. His idea was to adopt some ideas from type theory while being classical, and giving up on the idea that the program you want will emerge from a natural proof. He was convinced (and I agree) that you are better off allowing the user to supply the program, which sounds a bit like what you are requesting. But nobody has touched this in 35 years. It's there if you want to take a look.

Larry

On 7 Aug 2025, at 11:35, Andrea Vezzosi <vezzosi.ndr@gmail.com> wrote:

Are there Isabelle tools or formalizations in the area of program synthesis?

Especially interested in ones for functional languages (e.g. (some subset of) Haskell or ML), the end goal would be a tactic that given a specification and a partial program (i.e. with placeholders, aka typed holes) produces a completed program, if possible.

No particular constraints on the specification format, but the synthesis should be flexible in the form of programs that could be synthesized, because I would like to support a variety of partial programs as inputs.

Last updated: Aug 20 2025 at 20:23 UTC