Cette thèse se propose de rendre compte de l’articulation qui est opérée dans l’œuvre de Theodor W. Adorno entre critique de l’idéalisme et critique de la société. Ceci en confrontant deux figures que nous considérons comme centrales pour son dispositif : celle de principe d’identité et celle de société d’échange. Car il s’agit pour Adorno de déterminer la manière dont la logique de le pensée identifiante peut rencontrer celle de l’abstraction marchande : une même tendance à la mutilation de l’hétérogène y serait repérable. La question étant ici celle d’analyser comment ces deux modalités peuvent se médiatiser, de comprendre comment une philosophie orientée en direction du primat de la non-identité peut aussi dans le même temps se déployer comme théorie critique. En d’autres termes, saisir une contrainte objective dans et par le concept implique chez Adorno de rendre compte de l’imbrication entre idéalisme et domination sociale : de la critique de la logique conceptuelle identificatoire à celle de l’immanence du monde devenu système, en passant par celle de la subjectivité constituante ou des formes d’abstraction sociales fétichistes et réifiées. Tout l’enjeu de notre travail sera de ce fait de reconstruire les principales modalités d’une telle problématique, nous concentrant sur la discussion par Adorno des thèses d’Alfred Sohn-Rethel dans un premier temps, pour ensuite étudier selon deux grands moments le statut du principe d’échange et sa liaison avec la rationalité identificatoire ‒ celui de la Dialectique de la Raison (1944-47) et celui de la Dialectique négative (1966). / The aim of this dissertation is to account for the articulation between the critique of idealism and the critique of society operated in Theodor W. Adorno’s work. In order to do so, I compare two figures which I consider central in his conceptual apparatus : the identity principle and the exchange society. For Adorno’s goal is to determine the way the logic of identificatory thought meets the logic of commodity abstraction, where a same tendency towards the mutilation of the heterogeneous is at work. The question is thus to analyse how these two modalities can mediate each other and to understand how a philosophy which is guided by the primacy of non-identity can, at the same time, deploy itself as a critical theory. In other words, to grasp conceptually an objective constraint means for Adorno to account for the interweaving of idealism and social domination : from the critique of the indentificatory conceptual logic to the critique of the immancence of a now system-like world, through the critique of constitutive subjectivity and of forms of social, fetishistic and reified abstractions. The aim of this study is to reconstruct the main modalities of this problematic, focusing on Adorno’s dicussion of Alfred Sohn-Rethel first, and then on the status of the exchange principle and its connection witch identificatory rationality in Dialectic of Enlightenment (19944-47) and in Negative Dialectic (1966).

La vérification automatique de preuves consiste à faire vérifier par un ordinateur la validité de démonstrations d'énoncés mathématiques. Cette vérification étant purement calculatoire, elle offre un haut degré de confiance. Elle est donc particulièrement utile pour vérifier qu'un logiciel critique, c'est-à-dire dont le bon fonctionnement a un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens, correspond exactement à sa spécification. DEDUKTI est l'un de ces vérificateurs de preuves. Il implémente un système de type, le lambda-Pi-Calcul Modulo, qui est une extension du lambda-calcul avec types dépendants avec des règles de réécriture du premier ordre. Suivant la correspondance de Curry-Howard, DEDUKTI implémente à la fois un puissant langage de programmation et un système logique très expressif. Par ailleurs, ce langage est particulièrement bien adapté à l'encodage d'autres systèmes logiques. On peut, par exemple, importer dans DEDUKTI des théorèmes prouvés en utilisant d'autres outils tels que COQ, HOL ou encore ZENON, ouvrant ainsi la voie à l'interopérabilité entre tous ces systèmes. Le lambda-Pi-Calcul Modulo est un langage très expressif. En contrepartie, certaines propriétés fondamentales du système, telles que l'unicité des types ou la stabilité du typage par réduction, ne sont pas garanties dans le cas général et dépendent des règles de réécriture considérées. Or ces propriétés sont nécessaires pour garantir la cohérence des systèmes de preuve utilisés, mais aussi pour prouver la correction et la complétude des algorithmes de vérification de types implémentés par DEDUKTI. Malheureusement, ces propriétés sont indécidables. Dans cette thèse, nous avons donc cherché à concevoir des critères garantissant la stabilité du typage par réduction et l'unicité des types et qui soient décidables, de manière à pouvoir être implémentés par DEDUKTI. Pour cela, nous donnons une nouvelle définition du lambda-Pi-Calcul Modulo qui rend compte de l'aspect itératif de l'ajout des règles de réécriture dans le système en les explicitant dans le contexte. Une étude détaillée de ce nouveau calcul permet de comprendre qu'on peut ramener le problème de la stabilité du typage par réduction et de l'unicité des types à deux propriétés plus simples, qui sont la compatibilité du produit et le bon typage des règles de réécriture. Nous étudions donc ces deux propriétés séparément et en donnons des conditions suffisantes effectives. Ces idées ont été implémentées dans DEDUKTI, permettant d'augmenter grandement sa généralité et sa fiabilité. / Automatic proof checking is about using a computer to check the validity of proofs of mathematical statements. Since this verification is purely computational, it offers a high degree of confidence. Therefore, it is particularly useful for checking that a critical software, i.e., a software that when malfunctioning may result in death or serious injury to people, loss or severe damage to equipment or environmental harm, corresponds to its specification. DEDUKTI is such a proof checker. It implements a type system, the lambda-Pi-Calculus Modulo, that is an extension of the dependently-typed lambda-calculus with first-order rewrite rules. Through the Curry-Howard correspondence, DEDUKTI implements both a powerful programming language and an expressive logical system. Furthermore, this language is particularly well suited for encoding other proof systems. For instance, we can import in DEDUKTI theorems proved using other tools such as COQ, HOL or ZENON, a first step towards creating interoperability between these systems.The lambda-Pi-Calculus Modulo is a very expressive language. On the other hand, some fundamental properties such as subject reduction (i.e., the stability of typing by reduction) and uniqueness of types are not guaranteed in general and depend on the rewrite rules considered. Yet, these properties are necessary for guaranteeing the coherence of the proof system, but also for provingthe soundness and completeness of the type-checking algorithms implemented in DEDUKTI. Unfortunately, these properties are undecidable. In this thesis, we design new criteria for subject reduction and uniqueness of types that are decidable in order to be implemented in DEDUKTI.For this purpose, we give a new definition of the lambda-Pi-Calculus Modulo that takes into account the iterative aspect of the addition of rewrite rules in the typing context. A detailed study of this new system shows that the problems of subject reduction and uniqueness of types can be reduced to two simpler properties that we call product compatibility and well-typedness of rewrite rules.Hence, we study these two properties separately and give effective sufficient conditions for them to hold.These ideas have been implemented in DEDUKTI, increasing its generality and reliability.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Dans cette thèse, nous œuvrons à résoudre une énigme en implémentant une recherche en cours d’action : comment un dispositif pédagogique instrumenté complexe – DPIC – est devenu un service pédagogique instrumenté complexe – SPIC ? Et plus précisément : quels sont les ingrédients qui ont participé à l’effectivité du couplage d’une université et d’un environnement numérique de formation et comment étudier ces modes d’émergence et d’existence dans un registre méso organisationnel et décisionnel au niveau du mésosystème ? Cette énigme est résolue en mobilisant le DPIC comme un objet frontière et des outils épistémiques et méthodologiques tels que l’approche dispositive, l’approche écologique/systémique et la théorie de l’activité. L’analyse consiste à réaliser une lecture holistique de l’histoire. Cette approche méthodologique met en évidence la propension d’un dispositif à générer des objets définis comme connexes. L’exploration des propriétés de ces objets connexes démontre qu’il est possible de définir un continuum historique et de défaire les discontinuités inhérentes aux traces informatiques laissées par l’activité. / In this thesis, we are working to solve an enigma by implementing a “research in action”: how has complex instrumented educational dispositif – CIED – become complex instrumented educational service – CIES ? And more specifically: what are the ingredients that have participated in the effectiveness of the coupling of a university and a learning management system and how can we study the modes of emergence and existence in a meso organizational and decisional register and at the mesosystem class ?This enigma is solved by mobilizing the CIED as a boundary object and epistemological and methodological tools such as: the dispositive approach, the ecological / systemic approach and activity theory. The analysis involves achieving a holistic reading of history. This methodological approach highlights the propensity of a dispositif to generate objects defined as related objects. The exploration of the properties of these related objects shows that it is possible to define a historical continuum and undo the discontinuities of the activity inherent in the computer traces.

La thèse propose une théorie du discours de l’avocat devant la Cour de cassation. Plus précisément, c’est une partie du contenu de ce discours, les moyens de cassation, qui sont au cœur de l’analyse. Trop souvent, l’attention des théoriciens du droit se porte sur les discours qui sont traditionnellement perçus comme normatifs, à savoir le discours législatif et le discours jurisprudentiel. Assimilé au discours doctrinal parce qu’il n’est ni scientifique, ni à l’origine d’une norme, le discours de l’avocat demeure quant à lui dans une catégorie (les discours de « politique juridique » selon Kelsen, et les discours de « dogmatique juridique » selon Michel Troper) vouée à l’indifférence. Pourtant, ce n’est parce que les interprétations des avocats sont des actes guidés par la seule volonté de leurs auteurs qu’elles ne gagnent pas à faire l’objet d’une étude scientifique. Certains discours universitaires, également prescriptifs, font l’objet d’analyse visant à montrer leur incidence sur l’évolution de la jurisprudence alors même que d’un point de vue ontologique, le discours de l’avocat est mieux doté pour agir sur l’œuvre jurisprudentielle, notamment lorsqu’il est, comme celui de l’avocat aux Conseils, immédiatement et systématiquement destiné aux juridictions suprêmes. Cette spécificité du discours étudié, dégagée à travers l’étude de sa nature, nous permettra d’en étudier la portée. De ce point de vue, notre thèse, qui doit s’entendre comme une contribution à la théorie réaliste de l’interprétation et à son complément, la théorie des contraintes juridiques, propose une explication de la cohérence jurisprudentielle. Si la Cour de cassation, alors même qu’elle est libre d’interpréter les énoncés législatifs comme elle le souhaite (proposition centrale de la TRI), se montre généralement cohérente par rapport à sa jurisprudence antérieure, c’est parce qu’un ensemble de contraintes spécifiquement juridiques la conduisent à être cohérente (proposition centrale de la TCJ). Or, ces contraintes sont principalement produites ou relayées par les moyens de cassation (notre proposition). Sauf à relever un moyen d’office, procéder à une substitution de motifs ou énoncer un obiter dictum, techniques qui seront exceptionnellement utilisées par cet homo juridicus, la Cour de cassation est généralement contrainte d’effectuer un choix binaire, prédéterminé par le moyen de cassation : réaffirmer l’interprétation des juges du fond (arrêt de rejet) ou retenir celle de l’avocat du demandeur (arrêt de cassation). Autrement dit, le moyen de cassation définit le cadre de l’interprétation authentique, cadre qui favorise la circulation de la jurisprudence antérieure, et qui contraint la Cour de cassation à agir de façon prévisible. / In France, legal realism is currently represented by Michel Troper who is supporting the fact that the law resides in its interpretations by the Supreme Court. Supreme Court interpret legal text with complete freedom because those text do not contain any significations that necessarily need to be apply. This freedom regarding legal text does not exclude the existence of specific legal constraints which determine the supreme Court decisions. Even tough the lawyer’s discourse addressed to supreme jurisdictions does not look like any other legal discourses, it has never been apprehended as a source of constraint limiting sovereign courts freedom. This is what about I will discuss on my thesis.

Cette étude entend questionner l’impensé de la lecture et de la textualité sous-jacent aux modèles traductologiques orientés vers le processus qui se sont imposés en didactique de la traduction au cours des quatre dernières décennies, tels que la théorie interprétative de l’École de Paris et la théorie fonctionnaliste du Skopos de l’École allemande, et qui sous-tendent actuellement la formation des traducteurs professionnels au Canada. On trouvera dans ces pages, après un survol de l’histoire de cette formation, une confrontation dialogique entre les fondements immanentistes des approches qui y sont dominantes et ceux de théories issues du champ littéraire ayant problématisé l’acte de lecture, ainsi que l’analyse de la traduction collective d’une œuvre de fiction (réalisée par une équipe de traducteurs diplômés du premier cycle) dont le but est d’étayer la critique métathéorique.

L’objectif central de cette thèse est d’observer et de décrire le processus de naissance et d’institutionnalisation d’une nouvelle théorie de la peine : la théorie de la dénonciation. Cette théorie de la peine va naître à l’intérieur d’un système d’idées formé par d’autres théories de la peine déjà institutionnalisées. Ce système d’idées a été identifié et appelé par Alvaro Pires la « rationalité pénale moderne ». Notre contribution visera, elle, à observer d’une part le processus de naissance d’une autre théorie de la peine à l’intérieur de ce système d’idées et, d’autre part, la naissance et l’institutionnalisation de cette théorie dans divers discours : la philosophie et la doctrine juridique, les rapports des commissions de réforme du droit ou encore dans la jurisprudence (canadienne). Au cours de cette observation, nous aurons également la possibilité de voir comment une conception alternative de la dénonciation est apparue, mais sans réussir à prendre la forme stricte d’une « théorie de la peine » ni à s’institutionnaliser de façon stable et visible. Il s’agit de la dénonciation telle que l’a conçue la Commission de réforme du droit du Canada dans les années 1970. Cette manière de concevoir la dénonciation se situait à l’extérieur du système d’idées formé par la rationalité pénale moderne. Cette thèse fait plusieurs contributions à la fois, et de différents genres. Elle prétend contribuer entre autres à la description du processus de naissance et d’institutionnalisation d’une théorie (de la peine) du système de droit criminel en mettant en évidence comment cette théorie va s’opposer à une conception alternative portant le même nom et prédominer sur cette dernière. De plus, cette thèse va construire trois niveaux parallèles d’observation empirique. En effet, nous allons observer la naissance de cette théorie sur trois trames discursives distinctes et bien différenciées : (i) le discours de la philosophie, de la théorie du droit et de la sociologie (ou criminologie) ; (ii) le discours des commissions de réforme (« étatiques » et « non étatiques ») ; (iii) le discours de la jurisprudence.

On trouve dans la littérature de nombreux exemples de jeux où les stratégies souhaitées sont soumises à des contraintes ''transversales'' portant sur des ensembles de parties, reliées entre elles par quelque relation sémantique. L’exemple le plus fameux est celui des stratégies dans les jeux à information imparfaite, et les jeux où la condition de gain a un aspect épistémique en sont d’autres. Cependant, aucune étude approfondie n’a à notre connaissance été menée sur ce type de contraintes dans leur généralité. C’est ce que nous nous proposons de commencer dans cette thèse. Nous définissons donc une notion générale de stratégies uniformes. Les propriétés d’uniformité des stratégies sont exprimées dans un langage logique qui étend CTL∗ avec deux quantificateurs originaux. Ces quantificateurs sont très proches des opérateurs de connaissance classiques en logique épistémique, et font intervenir des ensembles de parties reliées entre elles par des relations binaires. Nous montrons comment cette notion de stratégies uniformes capture les exemples connus de la littérature, puis nous étudions en profondeur le problème de la synthèse de stratégies uniformes, en considérant que les relations binaires entre les parties sont reconnaissables par des automates finis (relations rationnelles). Nous établissons plusieurs résultats de décidabilité et de complexité, reposant largement sur des techniques d’automates : nous introduisons notamment comme outils les automates d’arbres bondissants et les automates d’ensembles d’informations. Par ailleurs, nos résultats permettent d’améliorer des résultats existants et d’en établir de nouveaux, dans les domaines du model-checking des logiques temporelles et épistémiques, ainsi que de la planification épistémique. / There are in the literature many examples of games where the desired strategies are submitted to ''transversal'' constraints involving sets of plays, related by some semantic relation. The most famous example is strategies for games with imperfect information, and games where the objective involves some epistemic aspect provide many more examples. Nevertheless, to the best of our knowledge, there has been no thorough study on this type of constraints in their generality. This is what this thesis intends to start. Therefore, we define a general notion of uniform strategies. Uniformity properties of strategies are expressed in a logical language that extends CTL∗ with two original quantifiers. These quantifiers are very close to the classic knowledge operators of epistemic logics, and they involve sets of plays related by binary relations. We show how this notion of uniform strategies captures the known examples from the literature, and we study in depth the problem of uniform strategy synthesis, assuming that the binary relations between plays can be recognized by finite automata (rational relations). We establish several decidability and complexity results, relying widely on automata techniques: in particular, we introduce as tools jumping tree automata and information sets automata. Moreover, our results enable us to improve existing results and establish new ones, in the domains of model checking epistemic temporal logics, and epistemic planning.

L'étude des processus de création de connaissances souligne la complexité des interactions individuelles au sein des organisations productives. Cette complexité est telle que les théories de l'entreprise basées sur les incitations, focalisées sur les problèmes de traitement de l'information, peuvent ignorer une part substantielle des facteurs de décision individuels intervenant dans le contexte de l'apprentissage organisationnel, et plus largement dans les processus de production collectifs. Nous utilisons dans cette thèse la méthode expérimentale pour étudier les déterminants de la coopération, afin d'affiner les hypothèses comportementales sur lesquelles sont basées les théories économiques de la production collective. Nous montrons que les deux visions de la coopération portées par les théories de l'entreprise - un comportement devant être extrait d'intérêts divergents et une propriété émergente découlant des interactions sociales entre agents – sont étayées par les résultats expérimentaux. Par conséquent, nous concluons que les deux approches devraient être retenues et éventuellement intégrées dans un cadre d'analyse plus large. / The study of knowledge creation processes has pointed to the complexity of individual interactions within productive organizations. This complexity appears to be such that incentive-based theories of the firm, which focus on information processing issues, may fail to grasp a substantial part of the individual decision-making involved in the context of organizational learning, and more broadly in collective production processes. In this thesis we use experimental methods to study the determinants of cooperation, in order to refine the behavioral assumptions on which economic theories of collective production are based. We show that the two visions of cooperation embodied in competing theories of the firm - a behavior to be elicited from diverging interests and an emergent property stemming from social interactions among agents - find support from the laboratory experiments. Accordingly, we conclude that both approaches should be upheld and possibly combined in a broader, integrative, analytical framework.

La théorie des cordes est un de nos meilleurs candidats pour une théorie quantique de la gravité. A ce jour elle n'a pas encore été conclusive à propose de ce sujet. Malgré cela, on a réalisé qu'on peut en tirer des informations sur tout une variété de sujets, dont notamment les théories de jauges supersymétriques, en étudiant la limite de basse énergie dans le volume d'univers des branes. Cette immersion des théories de jauges en théorie des cordes nous fournit un autre point de vue. Ce dernier nous permet souvent de prendre une approche plus géométrique pour obtenir de nouveaux résultats sinon inaccessible par des méthodes plus conventionnelles. Même en absence de vérification expérimentale de la supersymétrie, sa présence dans cette classe de théories de jauge nous fournit un terrain de jeux propice pour tester de nouvelles méthodes d'une manière efficace. En effet, la présence de la supersymétrie donne une structure additionnelle qui rend la théorie plus rigide. Cela simplifie les calculs et rend des résultats plus accessibles. On peut oser de dire que si on n'arrive pas à calculer un certain résultat en présence de supersymétrie, il y a très peu de chance d'y arriver sans. L'approche par la théorie des cordes le rend possible de découvrir des symétries cachées ou de comprendre des symétries connues d'une autre manière.Une classe de théories quantique intéressantes qui sont présentes en théories des cordes, c'est les théories de petites cordes. Ces dernières ont été découverte il y a deux décennies. Ces théories en six dimensions ont été construite une première fois comme théories dans le volume d'universe de branes NS5 dans le cadre de la théorie des cordes IIB en prenant la limite du couplage de la corde qui tend vers zéro. Dans cette limite, la théorie résultant reste non-trivial mais les interactions en dehors de la brane sont supprimées, notamment la gravité. Comme le nom le suggère, ces théories contiennent des cordes qu'on appelle petites cordes. La tension des petites cordes est proportionnelle à l'échelle naturelle de la corde. En plus, ces théories profitent de la T-dualité comme les théories de cordes critiques. Elle sont donc des théories quantiques non-locales. Leur complexité se situe entre celle des théories quantiques locales et celle de la théorie des cordes complète. Elles sont donc des candidates intéressantes pour étudier la dynamique dans le volume d'univers de la brane NS5. Pour des énergies inférieures à l'échelle de la corde, elles ont une description en termes de théories de jauges symétriques de type quiver. On peut donc également obtenir des informations sur ces dernières. Cette description locale n'est plus valable une fois l'échelle de la corde atteinte.Le but principal de cette thèse est d'étudier des dualités entre le théories de petites cordes en utilisant différentes constructions disponible en théorie des cordes. Cela nous permet d'attaquer le problème d'angles différents et de faire un lien avec des structures géométriques. En conséquence on peut analyser différentes relation parmi les théories de petites cordes. On confirme ensuite la validité des dualités qu'on obtient en utilisant la fonction de partition instantonique. Cet object est complètement non-perturbative et établit ces dualités comme résultat exact. Cette structure de dualités s'étend naturellement aux descriptions de basse énergie en terme de théories de jauges supersymétriques. De plus, on étudie les conséquences directes du réseaux de dualités qu'on a découvert. / String theory remains one of our best candidates for a theory of quantum gravity. Until now it has not lived up to this goal. However, along the way it was realized that string theory can give us valu-able insights into a variety of subjects among which supersymmetric gauge theories by studying the low-energy worldvolume dynamics of branes. This embedding of gauge theories into string theory provides us with a different viewpoint that often allows us to use powerful geometric considerati-ons in order to obtain new results that are inaccessible from conventional methods. Even in the ab-sence of experimental confirmation of supersymmetry, its presence in this class of gauge theories provides us with a playground where different methods can be tested in an efficient way. Indeed, supersymmetry provides additional structure, rendering the underlying theory more rigid and thus simplifying computations and making results more accessible. One could dare to say that when a certain result can not be calculated in the presence of supersymmetry, there is probably not much hope of achieving it without supersymmetry. This stringy approach to gauge theories makes it pos-sible to unravel hidden dualities or to understand already known ones from a different perspective. An interesting class of quantum theories that are embedded into string theory are the so called little string theories. They have been discovered two decades ago. These six-dimensional theories were first obtained as the worldvolume theory of a stack of NS5 branes in the context of Type II string theory trough a particular decoupling limit that sends the string coupling constant to zero while kee-ping at the same time the string scale finite. In this limit, the resulting theory remains interacting but the bulk dynamics is decoupled, in particular gravity. As their name suggests, they contain strings. The tension of the little strings is proportional to the string scale, which is the only intrinsic scale in the theory. Furthermore, the little string theories enjoy T-duality similar to the critical string theory. They are thus non-local quantum theories. So the complexity of little string theory lies between that of local quantum field theories and full fledged critical string theory. This makes them interesting candidates for studying stringy phenomena in an easier setup where gravity is absent and to learn more about the worldvolume dynamics of the NS5 brane. At energies far below the string scale, they have a low-energy description in terms of quiver gauge theories, so their study can also give us insights into these kinds of theories. This local description breaks down as we reach the string scale and we must rely on the full little string theories. The main goal of this thesis is to study dualities between little string theories by using different dual constructions available in string theory. These allow us to attack the problem from different angles and they establish also a connection to geometric structures. This makes it possible to systematically analyse relations among different little string theories. We then confirm the validity of the newly found duality relations by using the so called instanton partition function. The latter is a completely non-perturbative object allowing us to establish the dualities as an exact result. This duality structure naturally extends to the low-energy description in terms of supersymmetric quiver gauge theories. Furthermore, we study the direct consequences of this duality web. We find interesting cases where the dimensional reduction from six to five dimensions simultaneously reduces the rank of the group and changes the matter content. Another result that we find is the presence of a hidden dihedral symmetry which acts in a highly non-trivial fashion on the spectrum of the underlying gauge theories.