Verification of the optimizing phase of a compiler

计算机程序是使计算机执行某种任务的指令集。我们用人类容易理解的编程语言编写这些程序。然而，计算机是简单的，需要非常简单的指令来运行（例如，那些只涉及移动、加减数字的指令）。因此，为了使程序运行，我们需要将人类可读的程序转换为这些简单的指令。为了做到这一点，我们使用另一种称为编译器的计算机程序。重要的是，这个转换过程不会出错，否则计算机将不会做我们期望它做的事情。然而，编译器是非常复杂的程序，有时必须处理数百万条指令；很难知道翻译是否出了问题。而且，大多数编译器都很聪明，并在程序被翻译时尝试改进它。他们试图使程序更有效率，这使事情变得更加复杂，使人们更难知道翻译是否正确。幸运的是，计算机程序可以被视为数学对象（如数字、公式和方程），因此我们可以证明有关它们的事情。这项研究旨在找到证明编译器不会出错的方法——它们总是做正确的翻译。特别是，该研究着眼于如何在编译器试图改进程序时证明这一点。

Computer programs are sets of instructions to make a computer perform a certain task. We write these programs in programming languages that are easy for humans to understand. Computers, however, are simple and want very simple instructions to run (for example, ones that involve just moving, adding or subtracting numbers). So to get programs to run, we need to convert our human readable programs into these simple instructions. To do this we use another computer program called a compiler.It is important that this conversion process does not go wrong - otherwise the computer will not do what we expect it to do. However, compilers are very complicated programs, sometimes having to deal with millions of instructions; it is very hard to know whether the translation is going wrong. Also, most compilers are clever and attempt to improve the program as it is translated. They try to make the program more efficient and that complicates things even further / making it even harder to know whether the translation is correct or not.Luckily, computer programs can be viewed as mathematical objects (like numbers, formulas and equations) and therefore we can prove things about them. This research aims to find ways to prove that compilers do not go wrong - they always do a correct translation. In particular, the research looks at how to prove this even when the compiler is trying to improve the program.