Dependent types offer a uniform foundation for both proof systems and programming languages. While the proof systems built with dependent types have become relatively popular, dependently typed programming languages are far from mainstream. One key issue with existing dependently typed languages is the overly conservative definitional equality that programmers are forced to use. When combined with a traditional typing workflow, these systems can be quite challenging and require a large amount of expertise to master. This thesis explores an alternative workflow and a more liberal handling of equality. Programmers are given warnings that contain the same information as the type errors that would be given by an existing system. Programmers can run these programs optimistically, and they will behave appropriately unless a direct contradiction confirming the warning is found. This is achieved by localizing equality constraints using a new form of elaboration based on bidirectional type inference. These local checks, or casts, are given a runtime behavior (similar to those of contracts and monitors). The elaborated terms have a weakened form of type soundness: they will not get stuck without an explicit counter example. The language explored in this thesis will be a Calculus of Constructions like language with recursion, type-in-type, data types with dependent indexing and pattern matching. Several meta-theoretic results will be presented. The key result is that the core language, called the cast system, "will not get stuck without a counter example"; a result called cast soundness. A proof of cast soundness is fully worked out for the fragment of the system without user defined data, and a Coq proof is available. Several other properties based on the gradual guarantees of gradual typing are also presented. In the presence of user defined data and pattern matching these properties are conjectured to hold. A prototype implementation of this work is available.

L'automatisation de certaines tâches et traitements d'information grâce aux outils numériques permet de réaliser des économies considérables sur nos activités. Le Web est une plateforme propice à la mise en place de tels outils : ceux-ci sont hébergés par des serveurs, qui centralisent les informations et coordonnent les utilisateurs, et ces derniers accèdent aux outils depuis leurs terminaux clients (ordinateur, téléphone, tablette, etc.) en utilisant un navigateur Web, sans étape d'installation. La réalisation de ces applications Web présente des difficultés pour les développeurs. La principale difficulté vient de la distance entre les postes client et serveur. D'une part, la distance physique (ou distance matérielle ) entre les machines nécessite qu'une connexion réseau soit toujours établie entre elles pour que l'application fonctionne correctement. Cela pose plusieurs problèmes : comment gérer les problèmes de latence lors des échanges d'information ? Comment assurer une qualité de service même lorsque la connexion réseau est interrompue ? Comment choisir quelle part de l'application s'exécute sur le client et quelle part s'exécute sur le serveur ? Comment éviter aux développeurs d'avoir à résoudre ces problèmes sans pour autant masquer la nature distribuée des applications Web et au risque de perdre les avantages de ces architectures ? D'autre part, l'environnement d'exécution est différent entre les clients et serveurs, produisant une distance logicielle. En effet, côté client, le programme s'exécute dans un navigateur Web dont l'interface de programmation (API) permet de réagir aux actions de l'utilisateur et de mettre à jour le document affiché. De l'autre côté, c'est un serveur Web qui traite les requêtes des clients selon le protocole HTTP. Certains aspects d'une application Web peuvent être communs aux parties client et serveur, par exemple la construction de morceaux de pages Web, la validation de données saisies dans les formulaires, la navigation ou même certains calculs métier. Cependant, comme les API des environnements client et serveur sont différentes, comment mutualiser ces aspects tout en bénéficiant des mêmes performances d'exécution qu'en utilisant les API natives ? De même, comment conserver la possibilité de tirer parti des spécificités de chaque environnement ? Les travaux de cette thèse ont pour but de raccourcir cette distance, tant logicielle que matérielle, tout en préservant la capacité à tirer parti de cette distance, c'est-à-dire en donnant autant de contrôle aux développeurs. / Thanks to information technologies, some tasks or information process can be automated, thus saving a significant amount of money. The web platform brings numerous of such digital tools. These are hosted on web servers that centralize information and coordinate users, which can use the tools from several kinds of devices (desktop computer, laptop, smartphone, etc.), by using a web browser, without installing anything. Nevertheless, developing such web applications is challenging. The difficulty mainly comes from the distance between client and server devices. First, the physical distance between these machines requires them to be networked. This raises several issues. How to manage latency ? How to provide a good quality of service even when the network is down ? How to choose on which side (client or server) to execute a computation ? How to free developers from addressing these problems without yet hiding the distributed nature of web application so that they can still benefit from their advantages ? Second, the execution environment is different between clients and servers. Indeed, on client-side the program is executed within a web browser whose API provides means of reacting to user actions and of updating the page. On server-side, the program is executed on a web server that processes HTTP requests. Some aspects of web applications can be shared between client and server sides (e.g. content display, form validation, navigation, or even some business computations). However, the APIs and environments are different between clients and servers, so how to share the same code while keeping the same execution performance as with native APIs ? How to keep the opportunity to leverage the specificities of a given platform ? This work aims at shortening this distance while keeping the opportunity to leverage it, that is while giving developers as much expressive power.