TypeScript (TS) has been growing in popularity since its release in October 2012. It is beingadopted by many tech companies who specialize in web development. However, migrating old JSprojects to TS can be challenging and time consuming which can prove problematic due to limitedtime at the developers’ disposal.The aim of this study is to find out what the benefits of using TS over JS are, and their relationto Software Sustainability. By developing a migration tool that helps with automating the migrationprocess we investigate if such a tool would bring benefits to Axis Communications AB; especially,their web developers who work with JS and TS.After the development of the artifact, a focus group consisting of six experienced web developersand one tester was invited to a workshop in order to evaluate it. The workshop consisted of threeparts: Five open questions, a demo presentation of the artifact, and an artifact evaluation basedon the system dimensions: goal, environment, structure, activity, and evolution, by using the fivepoints Likert scale.Results from the workshop allowed us to understand better the needs and the challenges faced byAxis developers during software maintenance. Furthermore, the results indicated that the artifactnot only helps with improvements in terms of code maintenance but also indirectly improves codegreenability which in itself lowers CO2 emissions as a result.Migrating JS to TS improves some aspects of code maintenance and maintainability, and ourartifact helps with the automation of that migration process. With JavaScript, companies have tobalance sustainability with greenability. Fortunately, by adding green maintenance practices andusing TypeScript it is easier to keep that stability.

La thèse contribue à l’étude du λ-calcul non-typé de Church, un système de réécriture dont la règle principale est la β-réduction (formalisant l’exécution d’un programme). Nous nous concentrons sur la sémantique dénotationnelle, l’étude de modèles du λ-calcul interprétant de la même façon les λ-termes β-convertibles. On examine la sémantique relationnelle, une sémantique sensible aux ressources qui interprète les λ-termes comme des relations avec les entrées regroupées en multi-ensembles. Nous définissons une classe de modèles relationnels, les modèles de graphe relationnels (rgm’s), que nous étudions avec une approche issue de la théorie des types et de la démonstration, par le biais de certains systèmes de types avec intersection non-idémpotente. D’abord, nous découvrons la plus petite et la plus grande λ–théorie (théorie équationnelle étendant la β-conversion) représentées dans la classe. Ensuite, nous utilisons les rgm’s afin de résoudre le problème de l’adéquation complète pour la λ–théorie observationnelle de Morris, à savoir l’équivalence contextuelle de programmes que l’on obtient lorsqu’on prend les β-formes normales comme sorties observables. On résoudre le problème de différentes façons. En caractérisant la β-normalisabilité avec les types, nous découvrons une infinité de rgm’s complètement adéquats, que nous appelons uniformément sans fond. Puis, nous résolvons le problème de façon exhaustive, en prouvant qu’un rgm est complètement adéquat pour l’observabilité de Morris si et seulement si il est extensionnel (il modèle l’ŋ-conversion) et λ-König. Moralement un rgm est λ-König si tout arbre récursif infini a une branche infinie témoignée par un type non-bien-fondé / This thesis is a contribution to the study of Church’s untyped λ-calculus, a term rewritingsystem having the β-reduction (the formal counterpart of the idea of execution of programs) asmain rule. The focus is on denotational semantics, namely the investigation of mathematical models of the λ-calculus giving the same denotation to β-convertible λ-terms. We investigate relational semantics, a resource-sensitive semantics interpreting λ-terms as relations,with their inputs grouped together in multisets. We define a large class of relational models,called relational graph models (rgm’s), and we study them in a type/proof-theoretical way, using some non-idempotent intersection type systems. Firstly, we find the minimal and maximal λ-theories (equational theories extending -conversion) represented by the class.Then we use rgm’s to solve the full abstraction problem for Morris’s observational λ-theory,the contextual equivalence of programs that one gets by taking the β-normal forms asobservable outputs. We solve the problem in different ways. Through a type-theoretical characterization of β-normalizability, we find infinitely many fully abstract rgm’s, that wecall uniformly bottomless.We then give an exhaustive answer to the problem, by showing thatan rgm is fully abstract for Morris’s observability if and only if it is extensional (a model of ŋ-conversion) and λ-König. Intuitively an rgm is λ-König when every infinite computable tree has an infinite branch witnessed by some type of the model, where the witnessing is a property of non-well-foundedness on the type.