Type Theory, Logic & Functional Programming