Decidability and proof systems for language-based noninterference relations