KIAM Main page Web Library  •  Publication Searh  Русский 

PhD Theses, Moscow, 2017
On the degree of: Candidate of Physical and Mathematical Sciences
Specialty: 05.13.11 - mathematical and software of computers, complexes and computer networks
Dissertation council: Д 002.024.01
Author: Grechanik S. A.
Proof of the properties of functional programs by the method of saturation by equalities
The aim of the work is to investigate the possibility of using a combination of equality saturation methods and multi-result supercompilation to identify and prove the properties of programs in a non-strict functional language of the first order. The present work shows that, based on the method of saturation with equalities and transformations from supercompilation, it is possible to construct a system of transformation of functional programs applicable for proving equivalence. It is shown that this avoids the problem associated with a combinatorial explosion of the number of functions that differ only in the order of the arguments. It was also shown that the principle of induction can be formulated as a special transformation that works within the framework of the saturation system.
functional programs, the method of saturation with equalities, supercompilation, multi-result supercompilation
Publication language: russian,  pages: 215
Research direction:
Programming, parallel computing, multimedia
Russian source text:
Export link to publication in format:   RIS    BibTex