Compiler Backend of a Language for Verified Scientific Computing

Student: Andrushchenko Anton

Educational Programme: Applied Mathematics and Information Science (Bachelor)

Final Grade: 9

Year of Graduation: 2024

In recent years, the demand for large amounts of verified scientific computations has grown noticeably. Ideally, the very fact of the program should be sufficient to verify the correctness of a given algorithm. This principle applies equally to application domains, such as data analysis, as well as to theoretically oriented tasks, such as theorem proving. The solution to the problem of verifiability of computations falls first of all on the programming language used. Existing programming languages face various problems in achieving the necessary degree of correctness of algorithms. In this paper, we propose a software solution for compiling an abstract syntax tree within the compiler of a new programming language, called Sanskrit, designed to combine best practices and approaches from different existing programming languages.

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