ESVERIFY: Verifying Dynamically-Typed Higher-Order Functional Programs by SMT Solving. - Christopher Schuster; Sohum Banerjea; Cormac Flanagan (IFL, 2018)