Clarus

LIVE

Representation of data structures with sharing and cycles

Goal

Extend the inductive definitions (as found in ML) to express cycles or memory sharing. This could for example allow to declare doubly linked lists without mutable structures.

This will be done by the introduction of a let rec keyword.

Readings

• Type-safe datastructures with cycles and sharing (in progress)
• A Categorical Semantics of let and letrec (PhD) (in progress)
• Expressible sharing for functional circuit description (todo)