Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language