Encoding logical theories of programs