Higher-order minimal function graphs

Abstract. We present a minimal function graph semantics for a higher-order functional language with applicative evaluation order. The semantics captures the intermediate calls performed during the evaluation of a pro-gram. This information may be used in abstract interpretation as a basis for proving the soundness of program analyses. An example of this is the “closure analysis ” of partial evaluation. Program flow analysis is concerned with obtaining an approximate but safe descrip-tion of a program’s run-time behaviour without actually having to run it on its (usually infinite) input data set. Consider a functional program. The meaning of a simple function definition f(x1,..., xk) = e is typically given by a semantic function M of type M[[f(x1,..., xk) = e]] : V k → V⊥ where V is a set of values. Denotational semantics traditionally proceeds by defining M[[p]] by recursion on syntax. Semantics-based program approximation can be don