Re: [isabelle] New AFP entry: Light-weight Containers

> Light-weight Containers
> Andreas Lochbihler
> This development provides a framework for container types like sets and maps
> such that generated code implements these containers with different (efficient)
> data structures. Thanks to type classes and refinement during code generation,
> this light-weight approach can seamlessly replace Isabelle's default setup for
> code generation. Heuristics automatically pick one of the available data
> structures depending on the type of elements to be stored, but users can also
> choose on their own. The extensible design permits to add more implementations
> at any time.
> To support arbitrary nesting of sets, we define a linear order on sets based on
> a linear order of the elements and provide efficient implementations. It even
> allows to compare complements with non-complements.

I can spell it out in three letters: Wow!



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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