Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Aug 19 2022 at 10:57):

From: Tobias Nipkow <nipkow@in.tum.de>
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.

http://afp.sourceforge.net/entries/Containers.shtml

view this post on Zulip Email Gateway (Aug 19 2022 at 10:57):

From: Peter Lammich <lammich@in.tum.de>
The link behind "Download Entry" in the afp is broken.

view this post on Zulip Email Gateway (Aug 19 2022 at 10:57):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Fixed now. Sorry about that.

Cheers,
Gerwin


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

view this post on Zulip Email Gateway (Aug 19 2022 at 10:58):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I can spell it out in three letters: Wow!

Florian
signature.asc


Last updated: Nov 21 2024 at 12:39 UTC