{'fraction_non_alphanumeric': 0.019576719576719578, 'fraction_numerical': 0.0, 'mean_word_length': 5.041533546325879, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Curry-Howard Term Calculi for Gentzen-Style Classical Logics

This thesis is concerned with the extension of the Curry-Howard Correspondence to classical logic. Although much progress has been made in this area since the seminal paper by Griffin, we believe that the question of finding canonical calculi corresponding to classical logics has not yet been resolved. We examine computational interpretations of classical logics which we keep as close as possible to Gentzen’s original systems, equipped with general notions of reduction. We present a calculus X i which is based on classical sequent calculus and the stronglynormalising cut-elimination procedure defined by Christian Urban. We examine how the notion of shallow polymorphism à la ML can be adapted to this calculus. We show that the intuitive adaptation of these ideas fails to be sound, and give a novel solution. In the setting of classical natural deduction, we examine the λμ-calculus of Parigot. We show that the underlying logic is incomplete in various ways, compared with a standard Gentzen-style presentation of classical natural deduction. We relax the identified restrictions, yielding a richer calculus (νλμ) with a new kind of binding explicitly representing first-class continuations. We examine the relationship between various existing control operators in the literature and the νλμ-calculus. We show that the μ-binding, along with our generalised reduction rules, performs the role of a delimited control operator. We define a mapping from X i to νλμ, preserving typings and reductions. We believe this is the first time a general notion of cut-elimination for classical sequent calculus has been encoded into a calculus based on a Gentzen-style presentation of classical natural deduction. This encoding allows various of our results from the previous chapters to be adapted from one paradigm to the other.