What even is compiler correctness?
In this post I precisely define common compiler correctness properties. Compilers correctness properties are often referred to by vague terms such as "correctness", "compositional correctness", "separate compilation", "secure compilation", and others. I m...
In this post I precisely define common compiler correctness properties. Compilers correctness properties are often referred to by vague terms such as “correctness”, “compositional correctness”, “separate compilation”, “secure compilation”, and others. I make these definitions precise and discuss the key differences. I give examples of research papers and projects that develop compilers that satisfy each of these properties. What is a Language Our goal is to give a generic definition to compiler correctness properties without respect to a particular compiler, language, or class of languages. We
Explore this link on the map →saved by
related reading
- Formally speaking, "Transpiler" is a useless word | Rachit Nigampeople.csail.mit.edu
- Thompson_1984_ReflectionsonTrustingTrust.pdfcs.cmu.edu
- A friendly introduction to machine learning compilers and optimizershuyenchip.com
- Why ML/OCaml are good for writing compilersflint.cs.yale.edu
- Google's Fully Homomorphic Encryption Compiler — A Primer || Math ∩ Programmingjeremykun.com
- Against Query Based Compilersmatklad.github.io
- Type system - Wikipediaen.wikipedia.org
- Rambles around computer sciencehumprog.org
- Foundational Integration Verification of Diverse Software and Hardware Components | MIT CSAILcsail.mit.edu
- Preservation of Speculative Constant-Time by Compilationeprint.iacr.org
- Building a Performant Compiler from Scratch — Bowen Chengbowencheng.dev
- What can we learn from how compilers are designed?tedinski.com