{'fraction_non_alphanumeric': 0.009082652134423252, 'fraction_numerical': 0.0, 'mean_word_length': 5.156424581005586, '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': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Proving Properties About a Lazy Functional Language with theCoq Proof Development

In this paper we use the Coq Proof Development System to prove properties of the operational semantics of a lazy functional language. Coq is an implementation of the Calculus of Inductive Constructions and provides goal-directed tactic-driven proof search. The semantics of the functional language are presented as a deductively deened reduction system. The main results we prove are a subject reduction or type soundness theorem and a normal form characterization theorem. The subject reduction property states that the reduction rules preserve types. The normal form theorem deenes a subset of expressions which may be the result of an evaluation and shows that all successful evaluations result in a term in this subset. Our formalization in Coq makes extensive use of inductive deenitions to deene many aspects of this functional language from the syntax of types and expressions to the inference rules for type assignment and evaluation. Many properties are then proved by structural induction over these objects.