> static type checking based on sequent calculus, one of the most powerful systems for typing in

Not exactly a common characteristic for Lisps