A formal semantics of the GraalVM intermediate representation

DOI10.1007/978-3-030-88885-5_8zbMath1497.68104arXiv2107.01815OpenAlexW3209237303MaRDI QIDQ2147184

Mark Utting, Brae J. Webb, Ian J. Hayes

Publication date: 22 June 2022

Full work available at URL: https://arxiv.org/abs/2107.01815

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Isabelle/HOL
• LLVM
• CakeML
• CompCert
• Vellvm
• GitHub
• GraalVM

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Formalizing the LLVM intermediate representation for verified program transformations
• The program dependence graph and its use in optimization
• Heaps and Data Structures: A Challenge for Automated Provers
• CakeML

This page was built for publication: A formal semantics of the GraalVM intermediate representation