Treffer: Comparing functional programs, or how to put λ-terms back in order ; Comparer des programmes fonctionnels, ou comment remettre les λ-termes en ordre ; Comparing functional programs, or how to put λ-terms back in order: A theory of program equivalences and preorders through meaning, evaluation orders and costs ; Comparer des programmes fonctionnels, ou comment remettre les λ-termes en ordre: Une théorie des équivalences et préordres de programmes, à travers les notions de sémantique, ordre d’évaluation et coût

Program equivalence is a central topic in the study of programming languages. Certifying that compiler transformations do not change the semantics of a program is needed to formally prove correct compilers.This thesis aims at further developing the theory of program equivalences for the untyped pure λ-calculus, on several viewpoints. We suggest to switch from program equivalences to program preorders, which is a usual switch in the study of programming languages but perhaps not something fully accepted at the level of the λ-calculus. We show that some central concepts in the λ-calculus may be reformulated to simple properties on preorders for λ-terms.Contextual equivalences are the most natural notion of comparison for programs: contextual comparison is about testing programs in any execution environment and checking that they behave in a similar way. This equivalence is mostly unusable to provide proof of equivalences for expressive enough programming languages, because of the universal quantification over execution environments---akin to testing for all possible inputs.We introduce a quantitative refinement of contextual equivalence, trying to obtain a cost-sensitive program equivalence as natural as contextual comparison. Interaction equivalence tests programs in any execution environment, checks that their behavior is similar but also takes into account the number of communications (or interactions) between the program and its environment.Finally, we explore program equivalences for another evaluation paradigm, namely call-by-value. Call-by-value is more efficient and closer to the actual evaluation mechanism used by programming languages despite it being less studied than the original evaluation of the λ-calculus. It leads to a wide range of program equivalences, usually studied with effects added to the language. We study it here in a pure setting and show that call-by-value is a rich framework with many different notions of equivalences.We provide a unifying view of all these program equivalences and ...