IMDEA Software

IMDEA initiative

Home > News > 2023 > Martín Ceresa presents his thesis: "Theory of Improvements with Effects", based on program optimization

April 25, 2023

Martín Ceresa presents his thesis: "Theory of Improvements with Effects", based on program optimization

Pic

PhD student, Martín Ceresa, visitor at IMDEA Software Institute, has defended his thesis at the National University of Rosario on April 5th, entitled: “Theory of Improvements with Effects”, directed by Dr. Mauro Javier Jaskelioff.

Optimizing programs is not an easy task. A transformation does not necessarily imply an improvement. Therefore, when modifying a program, it must be shown that the semantics of the program are preserved, and furthermore, it must be ensured that the transformation is really an optimization, that the execution of the program is improved.

Martin’s thesis shows that there are several possible interpretations for the programs, but not all of them allow the natural introduction of intensive properties of their execution. This separation between the interpretation of programs and their evaluation leads him to implement program evaluation in order to have information relevant to resource consumption.

Functional languages have clearer semantics than non-functional languages. Knowing this fact has allowed him to perform equivalence tests of programs, but they hide properties of the execution. This has been the main motivation in the research world for the development of improvement theories and Ceresa has been able to present for the first time a relational theory of functional program costs.

Martin successfully characterizes improvement theories for functional languages with algebraic effects. “On the one hand, we add more expressiveness to functional languages by introducing algebraic effects, a subset of computational effects. While on the other, following the literature, we identify the definition of inter-program enhancements as a refinement of observational equivalence.”

Ceresa concludes that the thesis raises the beginning of the research of the study of intensive property analysis on functional language with algebraic effects opening more questions than solutions, which gives rise to a long-term future in the field of research in this regard.