[isabelle] Nominal Code Generation

Hi Christian,

> An aside: I'm currently using localized ad-hoc overloading for a port of
> Nominal2's permutation type, where I use locales instead of type
> classes. The reason is that, if I understand correctly, when using
> Nominal datatypes I loose code generation... is that still true for
> Nominal2? For an existing term datatype of IsaFoR I want to have notions
> of "supports/set of variables" and "freshness". That is my intended
> application of the above mentioned port, to be found at.

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.)



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.