Execution of programs.
A program is executed together with an input file. First we execute the input file, which results in a list of function arguments. Then we check the function arguments against the main function parameters, ensuring that they match up to reordering: there must arguments for all and only the parameters, with values matching types and with sorts matching. The matching process results in a list of argument values for the main function, which is used to execute the main function and obtain a result.