This is more programming language theory, or, rather the PL-theory portion of formal methods, which is a small portion of formal methods research. Most formal methods research these days focuses on sound static analysis, model checking and concolic testing, techniques that are showing better scalability than the deductive methods favored by PL theorists.