When & Where: 4:00pm, Monday, February 14, 2011, Room 200 AKW
Abstract:
Can we overcome the dichotomy of reasoning and programming? The Curry-Howard equivalence between propositions and types (or alterniatively proofs and programs) seem to indicate that this is possible in principle, but has this foundational insight any practical consequences?
The recent success of languages like Agda and extensions of CICC (the core language of Coq) shows that programming with dependent types inspired by Martin-Loef's Type Theory may provide the answer. However, languages like CICC or Agda are extremely complex and hard to analyze metatheoretically. In the present talk we introduce πΣ a small core language for dependently typed programming, and show how more sophisticated programming constructs can be represented using only a few primitives. We also discuss some basic design issues related to πΣ.
Biography:
Thorsten Altenkirch received his PhD in 1983 from the University of Edinburgh, Scotland. Subsequently he was Researcher at Chalmers University, Sweden and Edinburgh and then lecturer at the Universities of Munich Germany and Nottingham, England. Since 2006 he is Reader (Associate Professor) at the University of Nottingham and cochair of the Functional Programming Laboratory. His main interests are Type Theory and constructive logic, Functional Programming, Applications of Category Theory and Quantum Programming.