{'fraction_non_alphanumeric': 0.02180028129395218, 'fraction_numerical': 0.0007032348804500703, 'mean_word_length': 5.213973799126638, '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}}
Consuming and Persistent Types for Classical Logic

We prove that type systems are able to capture exact measures related to dynamic properties of functional programs with control operators, which allow implementing intricate continuations and backtracking. Our type systems give the number of evaluation steps to normal form as well as the size of this normal form without any evaluation being needed. We focus on Parigot's λμ-calculus, a computational interpretation of classical natural deduction, and our type systems are based upon non-idempotent intersection and union types. We introduce two kinds of arrows: consuming ones, which type function applications that are evaluated/destroyed during reduction, and persistent ones, which type those that are never consumed. These two forms of arrows are the essential tool of our typing systems to deal with control operators, as we are going to show. The main contribution of this paper is a type framework capturing exact measures within the λμ-calculus for 3 different evaluation strategies, namely, head, leftmost-outermost and maximal, associated to the well-known notions of head, weak and strong normalization respectively. Moreover, this is done in a parametric way: we do not provide one type system for each reduction strategy, as it is usually done in the literature, but we give a unique typing system parametrizing key concepts and factorizing common proofs.