Type-theoretic functional semantics :

Program extraction

Extraction of function F is simple, since it doesn't contain any proof components. The interpreter is then obtained by

interp :: Command -> State -> State interp = fix F