Semantic theories of programs with nested interrupts