Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nominal Code Generation


view this post on Zulip Email Gateway (Aug 19 2022 at 11:32):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,

there has never been a systematic attempt to generate code for nominal
applications. I have two ideas currently:

a) Nominal Logic is about binders. Maybe a translation to something
binder-free like combinatory logic is feasible?

b) Nominal2 uses quotient types. Usually these can be executed,
typically using abstract datatypes.

To investigate this, we would need a simple yet not wholly trivial
example. On occasion I would be willing to have a look at this and see
how far we can get using existing infrastructure. (This is actually the
first part of the Berghofer Triple Approach:
1. Make some examples.
2. Glimpse the general idea.
3. Implement it.)

Cheers,
Florian
signature.asc


Last updated: Mar 29 2024 at 08:18 UTC