Program synthesis is a process that obtains an efficient program out of a specification, preserving its meaning. Fork algebras have been proposed as an algebraic basis for the construction of a program synthesis environment. These algebras have an expressive power that encompasses that of first order logic, and they are also the right abstraction of the set model that considers programs as partial binary relations; these results make fork algebras a sound and powerful framework for this task.An …
Read moreProgram synthesis is a process that obtains an efficient program out of a specification, preserving its meaning. Fork algebras have been proposed as an algebraic basis for the construction of a program synthesis environment. These algebras have an expressive power that encompasses that of first order logic, and they are also the right abstraction of the set model that considers programs as partial binary relations; these results make fork algebras a sound and powerful framework for this task.An important step in the software construction process is the correct selection and manipulation of datatypes, because they are a powerful tool - with them modularization is easy, and enhancement of readability and early error detection are obtained. Algebraic datatypes , are an important class of datatypes because their properties are of great relevance in program transformation.The main goals of this work are to provide a general mechanism for defining algebraic datatypes in the framework of fork algebras, and, at the same time, establish a syntax that simplifies the notation for the specifications
