Compiler Front-end of a Language for Verified Scientific Computing

Student: Karpyshev Sergei

Educational Programme: Applied Mathematics and Information Science (Bachelor)

Final Grade: 8

Year of Graduation: 2024

The verification problem always was relevant for the scientific researches. Modern programming languages such as Lean, Idris, Coq and others provide the opportunity to prove the logical correctness of the theorem proofs, but a complex numerical computing can be a hard problem for such instruments. There are more lower-level languages such as Scala that are giving more abilities for the computations by the cost of the verification. Our point is to make a compromise solution which allow wide computation capabilities alongside with the strong correctness proving at the same time. The idea is to use the functional based λ-calculus approach on the front-end compiler phase simultaneously with the efficient low-level computations on the back-end phase.

Full text (added May 20, 2024)

Student Theses at HSE must be completed in accordance with the University Rules and regulations specified by each educational programme.

Summaries of all theses must be published and made freely available on the HSE website.

The full text of a thesis can be published in open access on the HSE website only if the authoring student (copyright holder) agrees, or, if the thesis was written by a team of students, if all the co-authors (copyright holders) agree. After a thesis is published on the HSE website, it obtains the status of an online publication.

Student theses are objects of copyright and their use is subject to limitations in accordance with the Russian Federation’s law on intellectual property.

In the event that a thesis is quoted or otherwise used, reference to the author’s name and the source of quotation is required.

Search all student theses