- Canonicalizations
Canonicalization phase
- ConditionalElimination
(experimental) Conditional elimination phase
- Document
Whole project document
- Graph
GraalVM Intermediate Representation encoding
- OptimizationDSL
DSL for expressing optimizations
- Proofs
Supporting proof theories and definitions
- Semantics
Semantics of the GraalVM IR
- SemanticsPaper
Content for IR semantics description paper
- Snippets
Additional commands to enable the generation of LaTeX snippets of theories
- StampLattice
(experimental) Investigation of an alternative approach to representing stamps in Isabelle/HOL
- TreePaperSnippets
Snippets of Isabelle theories used for the preparation of the future paper ``Verifying term graph optimizations using Isabelle/HOL''
- ValidationPaperSnippets
Snippets of Isabelle theories used for the preparation of the future paper ``Validating Faithful Formalization of an Existing Compiler''