## Lvc.IL.Annotation

## Lvc.IL.IL

## Lvc.IL.Var

## Lvc.Equiv.Bisim

## Lvc.Equiv.TraceEquiv

- Divergence
- Three equivalent notions of program equivalence

## Lvc.Alpha

## Lvc.Liveness

- Liveness
- Inductive Definition of Liveness
- Relation between different overapproximations
- live_sound ensures that the annotation matches the program
- Some monotonicity properties
- Live variables always contain the free variables
- Liveness is stable under renaming
- For functional programs, only free variables are significant
- Since live variables contain free variables, liveness contains all variables significant to an IL/F program
- Live variables contain all variables significant to an IL/I program

## Lvc.Isa.Val

## Lvc.Isa.MoreExp

## Lvc.Isa.Exp

## Lvc.RenamedApart

## Lvc.Coherence.AllocationAlgo

## Lvc.Coherence.Allocation

- Local Injectivity
- Inductive definition of local injectivity of a renaming rho
- Some Properties
- local injectivity is decidable
- Renaming with a locally injective renaming yields a coherent program
- Theorem 6 from the paper.
- Renaming with a locally injective renaming yields an α-equivalent program
- Theorem 7 from the paper
- local injectivity only looks at variables occuring in the program

## Lvc.Coherence.Coherence

- Definition of Coherence: srd

## Lvc.Coherence.Restrict

## Lvc.Fresh

## Lvc.RenameApart

## Lvc.RenamedApart_Liveness

## Lvc.Alpha_RenamedApart

This page has been generated by coqdoc