Lvc.Equiv.WFBisim

• • • Bisimulation is an reflexive and symmetric
  • Relationship of bisimulation to the parametric definition

Lvc.Equiv.NonParametricBiSim

• Non-parametric Definitions of Simulation and Bisimulation
  • Bisimulation
    • Bisimulation is an reflexive and symmetric
  • Relationship of bisimulation to the parametric definition
    • Transitivity
  • Simulation
    • Simulation is an reflexive
  • Relationship of simulation to the parametric definition
    • Transitivity

Lvc.Equiv.SimI

• A Framework for Simulation Proofs by Induction: Imperative Version
  • Proof Relation
  • Parameter Relation and Separation
  • Application Relation
  • Label Environment Relation
  • Key Lemmata
    • Fix Compatibility
    • Extension Lemma
    • Fun Compatibility
    • Specialized Version if function bindings are not changed
    • A small study on IL fixed-points in general

Lvc.Equiv.SimCompanion

Lvc.Equiv.SimF

• A Framework for Simulation Proofs by Induction: Functional Version
  • Proof Relation
  • Parameter Relation and Separation
  • Application Relation
  • Label Environment Relation
  • Key Lemmata
    • Fix Compatibility
    • Extension Lemma
    • Fun Compatibility
    • Specialized Version if function bindings are not changed
    • A small study on IL fixed-points in general

Lvc.Equiv.CtxEq

• Program Equivalence
  • Reflexivity
• Contextual Equivalence
  • Program Equivalence is contextual

Lvc.Equiv.Tower3

Lvc.Equiv.Sim

• Parametric Definition of Simulation and Bisimulation
  • Generating Function
  • Reflexivity, Symmetry
  • Admissible Rules
  • Closedness under Expansion and Reduction
  • Transitivity

Lvc.Equiv.SimLockStep

• • Reflexivity, Symmetry

Lvc.Equiv.TraceEquiv

• Divergence
  • Bisimilarity preserves silent divergence
  • Silently diverging programs are bisimlar
• Prefix Trace Equivalence (partial traces)
  • Bisimilarity is sound for prefix inclusion
  • The only prefix is empty if and only if the state diverges
  • Prefix Equivalence is sound for divergence
  • Several closedness properties
• Trace Equivalence (maximal traces)
  • Several closedness properties
  • Bisimilarity is sound for maximal traces
  • Prefix trace equivalence coincides with maximal trace equivalence.
  • Bisimilarity is complete for prefix trace equivalence.

Lvc.Equiv.Tower2

Lvc.Equiv.SimTactics

• Admissible Rules and Tactics
  • Tactics
  • Admissible Rules
    • Conditional Elimination

Lvc.Equiv.TraceEquivSim

Lvc.Constr.MapDecidable

Lvc.Constr.MapAgreement

Lvc.Constr.CMapPartialOrder

Lvc.Constr.CSetTac

Lvc.Constr.MapAgreeSet

Lvc.Constr.CMapDomain

Lvc.Constr.CSetNotation

Lvc.Constr.MapInjectivity

Lvc.Constr.MapBasics

Lvc.Constr.MapLookupList

Lvc.Constr.MapLookup

Lvc.Constr.MapInverse

Lvc.Constr.CMapTerminating

Lvc.Constr.CSetComputable

Lvc.Constr.MapComposition

Lvc.Constr.CSetBasic

Lvc.Constr.CMap

Lvc.Constr.CSetGet

Lvc.Constr.CSetCases

Lvc.Constr.CSetPartialOrder

Lvc.Constr.MapUpdate

Lvc.Constr.CSetDisjoint

Lvc.Constr.PairwiseDisjoint

Lvc.Constr.CSet

Lvc.Constr.CMapJoinSemiLattice

Lvc.Constr.ElemEq

Lvc.Constr.SetOperations

Lvc.Constr.Map

Lvc.Constr.MapDefined

Lvc.DVE

• Dead Variable Elimination
  • Correctness with respect to the imperative semantics IL/I
  • Correctness with respect to the functional semantics IL
  • Reconstruction of Liveness Information after DVE
  • DVE and Unreachable Code

Lvc.RegAssign

Lvc.Alpha.RenameApart

Lvc.Alpha.RenamedApartAnn

Lvc.Alpha.RenamedApart

• Renamed-apart (formally)
  • Morphisms
  • Relation to freeVars and occurVars
  • The two annotating sets are disjoint.

Lvc.Alpha.RenameApart_Liveness

Lvc.Alpha.RenameApart_Partition

Lvc.Alpha.RenameApart_Alpha

Lvc.Alpha.Alpha_RenamedApart

• Properties of Alpha Equivalence and Renamed Apart Programs
  • Given an renamedApart program, every alpha-equivalent program
  • Alpha Equivalent programs map to identical De-Bruijn terms

Lvc.Alpha.ShadowingFree

Lvc.Alpha.RenamedApart_Liveness

Lvc.Alpha.RenameApart_VarP

Lvc.Alpha.Alpha

• Alpha Equivalence
  • Morphisims
  • Properties
    • ϱ and ϱ' are inverses of each other on the free variables of s
    • Reflexivity
    • Symmetry
    • Transitivity
  • Soundness wrt. equivalence

Lvc.Compiler

Lvc.DCVE

Lvc.Spilling.ReconstrLive

• ReconstrLive

Lvc.Spilling.SpillSound

• Correctness Predicate with 5 inference rules

Lvc.Spilling.SimpleSpill

• SimpleSpill

Lvc.Spilling.RegisterBound

• RegisterBound

Lvc.Spilling.ReconstrLiveSound

• ReconstrLiveSound

Lvc.Spilling.Slot

• Slot

Lvc.Spilling.DoSpillRm

• DoSpillRm

Lvc.Spilling.SpillUtil

• SpillUtil

Lvc.Spilling.SetUtil

• SetUtil

Lvc.Spilling.AnnP

• AnnP

Lvc.Spilling.OneOrEmpty

Lvc.Spilling.DoSpill

Lvc.Spilling.ExpVarsBounded

• ExpVarsBounded

Lvc.Spilling.LiveMin

Lvc.Spilling.RLiveMin

Lvc.Spilling.SlotLiftArgs

Lvc.Spilling.RepairSpillIdem

• Idempotence of repair_spill with reg_live

Lvc.Spilling.SpillMaxKill

Lvc.Spilling.RepairSpillInv

• Invariance on correct spillings

Lvc.Spilling.ReconstrLiveSmall

• ReconstrLiveSmall

Lvc.Spilling.InVD

• InVD

Lvc.Spilling.VarInRegister

• VarInRegister

Lvc.Spilling.RegLive

• Register Liveness

Lvc.Spilling.SpillSim

• SpillSim

Lvc.Spilling.PickLK

Lvc.Spilling.SlotLiftParams

• DoSpill

Lvc.Spilling.SplitSpill

• SplitSpill

Lvc.Spilling.RepairSpillSound

• Soundness of repair_spill

Lvc.Spilling.BoundedIn

• BoundedIn

Lvc.Spilling.RLiveSound

Lvc.Spilling.SpillMovesAgree

Lvc.Spilling.ToBeOutsourced

• ToBeOutsourced

Lvc.Spilling.ReconstrLiveG

• ReconstrLiveG

Lvc.Spilling.RepairSpill

• Repair Spill

Lvc.Spilling.ReconstrLiveUtil

• ReconstrLiveUtil

Lvc.Spilling.Spilling

• Spilling

Lvc.Spilling.SpillSoundSeven

• Correctness Predicate with 7 inference rules

Lvc.IL.ILN

• • • Functional Semantics
    • Imperative Semantics

Lvc.IL.LabelsDefined

Lvc.IL.Subterm

Lvc.IL.Events

• • filter_tau

Lvc.IL.ILN_IL

Lvc.IL.ILDB

• • • Functional Semantics

Lvc.IL.InRel

Lvc.IL.Sawtooth

Lvc.IL.Env

• Environments for Types and Values
  • Type Environments
  • Value Environments

Lvc.IL.StateType

Lvc.IL.BlockType

Lvc.IL.Patterns

Lvc.IL.Exp

• Extended Expressions
  • Renaming
  • Liveness
  • Alpha Equivalence

Lvc.IL.Annotation

Lvc.IL.InRel4

Lvc.IL.AppExpFree

Lvc.IL.Var

• Definitions related to variables
  • A class for counted types
  • Variables
  • Locations
  • Labels
    • equality of labels is decidable
    • labels are counted
  • lab

Lvc.IL.VarP

Lvc.IL.IL

• Intermediate Language IL
  • Syntax
    • Free, Defined and Occuring Variables
  • Semantics
    • Functional Semantics
    • Imperative Semantics

Lvc.IL.Rename

Lvc.IL.AnnotationLattice

Lvc.IL.SmallStepRelations

• • plus2 - transitive closure for event-labeled relations
  • plus2 - reflexive, transitive closure for event-labeled relations

Lvc.IL.ILStateType

Lvc.Isa.Op

• Operations

Lvc.Isa.BitVector

Lvc.Isa.Val

• More or less abstract values

Lvc.Isa.OrderedBitVector

Lvc.Analysis.ContextMap

Lvc.Analysis.Analysis

Lvc.Analysis.AnalysisForward

Lvc.Analysis.AnalysisBackward

Lvc.Analysis.AnalysisForwardSSA

Lvc.Analysis.DomainSSA

Lvc.Infra.Drop

Lvc.Infra.OptionMap

Lvc.Infra.StableFresh

Lvc.Infra.OUnion

Lvc.Infra.Sublist

Lvc.Infra.InfinitePartition

Lvc.Infra.Take

Lvc.Infra.Position

Lvc.Infra.MoreInversion

Lvc.Infra.DecSolve

Lvc.Infra.FiniteFixpointIteration

Lvc.Infra.WithTop

Lvc.Infra.LvcPlugin

Lvc.Infra.Terminating

Lvc.Infra.Option

Lvc.Infra.BoundedBelow

Lvc.Infra.OptionR

Lvc.Infra.Smpl

Lvc.Infra.Fresh

Lvc.Infra.SigR

Lvc.Infra.Subset1

Lvc.Infra.Util

• Reflecting boolean statements to Prop
• Omega Rewrite
• Misc. Tactics
  • List Length automation

Lvc.Infra.MapSep

Lvc.Infra.FreshGen

Lvc.Infra.Keep

Lvc.Infra.LengthEq

Lvc.Infra.SizeInduction

Lvc.Infra.MoreList

• Lemmas and tactics for lists

Lvc.Infra.ListUpdateAt

Lvc.Infra.Filter

Lvc.Infra.EqDec

• Wrapper for decidable equalities in coq.

Lvc.Infra.SafeFirst

Lvc.Infra.Len

Lvc.Infra.MoreTac

Lvc.Infra.PartialOrder

Lvc.Infra.MoreListSet

Lvc.Infra.Get

• Positional membership in a list
• Properties of get

Lvc.Infra.Indexwise

Lvc.Infra.TakeSet

Lvc.Infra.ListMax

Lvc.Infra.PE

Lvc.Infra.Lattice

Lvc.Infra.Status

• Reasoning over monadic computations

Lvc.Infra.Computable

• Classical reasoning on decidable propositions.

Lvc.Infra.AutoIndTac

Lvc.Infra.Range

Lvc.Infra.AllInRel

• AllInRel: Inductive characterization of lists which are element-wise in relation

Lvc.RenameApartToPart

Lvc.Liveness.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

Lvc.Liveness.LivenessAnalysisCorrect

Lvc.Liveness.LivenessValidators

Lvc.Liveness.LivenessCorrect

• • For functional programs, only free variables are significant
  • Live variables contain all variables significant to an IL/I program

Lvc.Liveness.LivenessAnalysis

Lvc.Liveness.TrueLiveness

• Specification of True Liveness
  • The inductive predicate
    • Some properties of the predicate

Lvc.Lowering.Renest

Lvc.Lowering.EAE

Lvc.Lowering.ParallelMove

• Parallel Moves

Lvc.UCE

• Unreachable Code Elimination
  • The transformer
    • Properties of the transformer
  • Correctness with respect to the imperative semantics IL/I
  • Correctness with respect to the functional semantics IL
  • UCE respects parameter/argument matching
  • Reconstruction of Liveness Information after UCE
  • Completeness of Reachability

Lvc.Reachability.ReachabilityAnalysis

Lvc.Reachability.ReachabilityAnalysisCorrect

Lvc.Reachability.Reachability

• Rechability Specification
  • The inductive predicate
  • Some Properties of the Predicate

Lvc.Reachability.ReachabilityAnalysisCorrectSSA

Lvc.Coherence.DelocationValidator

Lvc.Coherence.AllocationAlgoBound

Lvc.Coherence.AddAdd

Lvc.Coherence.DelocationAlgo

Lvc.Coherence.Invariance

• • Definition of invariance
  • Agreement Invariant
  • Main Theorem about Coherence
  • Context coherence for IL/F contexts: approxF
  • Coherence implies invariance

Lvc.Coherence.Allocation

• Local Injectivity
  • Inductive definition of local injectivity of a renaming rho
  • Some Properties
  • 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
  • Liveness is stable under renaming with locally injective renaming

Lvc.Coherence.DelocationCorrect

Lvc.Coherence.AllocationValidator

• • Coherence is decidable
  • local injectivity is decidable

Lvc.Coherence.AllocationAlgo

• SSA-based register assignment formulated for IL

Lvc.Coherence.Coherence

• Definition of Coherence: srd
  • Some monotonicity properties
    • Every renamed apart program is coherent
    • In a coherent program, the globals of every function that can eventually be called are live
    • On a coherent program a liveness analysis which is sound imperatively is also sound functionally.

Lvc.Coherence.DelocationAlgoCorrect

Lvc.Coherence.AddParam

Lvc.Coherence.Delocation

• • DVE and Unreachable Code

Lvc.Coherence.DelocationAlgoLive

Lvc.Coherence.DelocationAlgoIsCalled

Lvc.Coherence.AllocationAlgoCorrect

• • the algorithm produces a locally injective renaming
  • Theorem 8 from the paper.

Lvc.Coherence.Restrict

Lvc.Coherence.AddParams