Title: Using typed Lambda calculus to implement formal systems on a machine