Output details
11 - Computer Science and Informatics
Queen Mary University of London
Hybrid functional interpretations of linear and intuitionistic logic
<11>The paper shows that, via the use of linear logic, distinct functional interpretations such as Gödel’s dialectica and Kreisel’s modified realizability can be combined – to achieve maximum benefit – when extracting information from proofs. This paper represents the culmination of my 5-year research programme on the unification of various functional interpretations. This research laid the foundations for a recent EPSRC grant on “Computation-sensitive Proofs”, and led to several invitations as plenary speaker for major European conferences in Logic and Computer Science (Computer Science Logic 2009, British Logic Colloquium 2009, Logic Colloquium 2010).