The Unfolding Semantics of Functional Programs

TL;DR

This paper develops an unfolding semantics for higher-order, lazy functional programs, providing a new way to analyze and understand their behavior with proven correctness and practical applications.

Contribution

It introduces the first unfolding semantics for higher-order, lazy functional languages and demonstrates its correctness and usefulness.

Findings

Proves the adequacy of the semantics with respect to operational semantics

Applies the semantics to static analysis and program characterization

Extends unfolding techniques to a new class of functional programs

Abstract

The idea of using unfolding as a way of computing a program semantics has been applied successfully to logic programs and has shown itself a powerful tool that provides concrete, implementable results, as its outcome is actually source code. Thus, it can be used for characterizing not-so-declarative constructs in mostly declarative languages, or for static analysis. However, unfolding-based semantics has not yet been applied to higher-order, lazy functional programs, perhaps because some functional features absent in logic programs make the correspondence between execution and unfolding not as straightforward. This work presents an unfolding semantics for higher-order, lazy functional programs and proves its adequacy with respect to a given operational semantics. Finally, we introduce some applications of our semantics.