COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Typed realizability for first-order classical analysis

## Typed realizability for first-order classical analysisAdd to your list(s) Download to your calendar using vCal - Valentin Blot, Mathematical foundations group, computer science department, University of Bath
- Friday 27 November 2015, 14:00-15:00
- FW26.
If you have a question about this talk, please contact Ohad Kammar. We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed lambda-mu-calculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to intuitionistic logic. We prove that the usual terms of Gödel’s system T realize the axioms of Peano arithmetic, and that under some assumptions on the computational model, the bar recursion operator realizes the axiom of dependent choice. We also perform a proper analysis of relativization, which allows for less technical proofs of adequacy. Extraction of algorithms from proofs of pi-0-2 formulas relies on a novel implementation of Friedman’s trick exploiting the control possibilities of the language. This allows to have extracted programs with simpler types than in the case of negative translation followed by intuitionistic realizability. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsOperations Group Seminar Series DAMTP Fluids Talks 'Expanding Horizons' - Cambridge MedSoc Talks MEMS ME Seminar Combined TCM Seminars and TCM blackboard seminar listing## Other talksPOSTPONED - Acoustics in the 'real world' - POSTPONED Regulation of progenitor cells in adult lung and in lung cancer Protean geographies: Plants, politics and postcolonialism in South Africa Investigation into appropriate statistical models for the analysis and visualisation of data captured in clinical trials using wearable sensors Regulators of Muscle Stem Cell Fate and Function International Snowballing and the Multi-Sited Research of Diplomats |