LVC
LVC is a verfied compiler which is based on the term-based intermediate language IL, a functional language with nested, mutually recursive definitions. IL replaces SSA's dominance criterion by term nesting with lexical scoping, hence we say IL realizes "Functional SSA".
In previous work we showed that SSA-based register allocation can be faithfully implemented on functional SSA.