Correct-by-Construction Typechecking with Scope Graphs