**math.LO Logic** * Lambda calculus, the theoretical basis for [functional programming][1] (Lisp in particular), was developed by Alonzo Church in the 1930's as part of his research on recursion and the foundations of mathematics. * [Formal verification][2] is used to verify software and hardware in which failure rates need to be as close to zero as possible (e.g. avionics) * [Finite Model Theory][3] is used to design and improve database query systems. [1]: http://en.wikipedia.org/wiki/Functional_programming [2]: http://en.wikipedia.org/wiki/Formal_verification [3]: http://homepages.inf.ed.ac.uk/libkin/papers/fmtpods09.pdf