Programming with Classical Proofs Hans Bugge Grathwohl Abstract: This thesis is about extracting programs from classical proofs. In the first part, we show conservativity of Peano arithmetic over Heyting arithmetic for Π02-sentences, an old result of Kreisel, using Friedman’s A-translation technique. Then we present some extensions by Parigot and Krebbers of the lambda-calculus with control mechanisms, that allow for some amount of classical reasoning via the Curry–Howard correspondence. In the second part of the thesis, we present a new system by Aschieri and Berardi, HA + EM1 , a Curry–Howard system for an arithmetic with a limited amount of classical reasoning that is based on ideas from their Interactive Realizability semantics for classical arithmetic. We show Aschieri’s recent proof of strong normalization of HA + EM1 that uses a new technique based on non-deterministic choice. Two non-trivial examples of proof terms in HA+EM1 are then worked out, and their possible reduction paths are analyzed. On basis of this, an operational natural semantics for HA + EM1 is developed and tested on the previous examples.