A Linear First-Order Functional Intermediate Language for Verified Compilers
From MaRDI portal
Publication:2945646
DOI10.1007/978-3-319-22102-1_23zbMath1465.68042arXiv1503.08665MaRDI QIDQ2945646
Sebastian Hack, Gert Smolka, Sigurd Schneider
Publication date: 14 September 2015
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1503.08665
Related Items
Verified spilling and translation validation with repair, A Linear First-Order Functional Intermediate Language for Verified Compilers
Uses Software
Cites Work
- Unnamed Item
- Optimal register allocation for SSA-form programs in polynomial time
- Concrete Semantics
- Formalizing the LLVM intermediate representation for verified program transformations
- A Linear First-Order Functional Intermediate Language for Verified Compilers
- Formal Verification of Coalescing Graph-Coloring Register Allocation
- A verified compiler for an impure functional language
- Correspondence between ALGOL 60 and Church's Lambda-notation