Email Gateway (Aug 19 2022 at 11:32): 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: Nov 21 2024 at 12:39 UTC