{'fraction_non_alphanumeric': 0.02558001189767995, 'fraction_numerical': 0.003569303985722784, 'mean_word_length': 4.2398753894081, '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}}
Proofs as Programs 3.1 Propositions as Types

In this chapter we investigate a computational interpretation of constructive proofs and relate it to functional programming. On the propositional fragment of logic this is referred to as the Curry-Howard isomorphism [How80]. From the very outset of the development of constructive logic and mathematics, a central idea has been that proofs ought to represent constructions. The Curry-Howard isomorphism is only a particularly poignant and beautiful realization of this idea. In a highly influential subsequent paper, Martin-Löf [ML80] developed it further into a more expressive calculus called type theory. In order to illustrate the relationship between proofs and programs we introduce a new judgment: M : A M is a proof term for proposition A We presuppose that A is a proposition when we write this judgment. We will also interpret M : A as " M is a program of type A ". These dual interpretations of the same judgment is the core of the Curry-Howard isomorphism. We either think of M as a term that represents the proof of A true, or we think of A as the type of the program M. As we discuss each connective, we give both readings of the rules to emphasize the analogy. We intend that if M : A then A true. Conversely, if A true then M : A. But we want something more: every deduction of M : A should correspond to a deduction of A true with an identical structure and vice versa. In other words we annotate the inference rules of natural deduction with proof terms. The property above should then be obvious. Conjunction. Constructively, we think of a proof of A ∧ B true as a pair of proofs: one for A true and one for B true.