L'apprentissage des preuves mathématiques déductives est fondamental dans l'enseignement des mathématiques. Pourtant, la dernière enquête TIMSS (Trends in International Mathematics and Science Study) menée par l'IEA ("International Association for the Evaluation of Educational Achievement") en mars 2015, le niveau général des étudiants en mathématiques est en baisse et les étudiants éprouvent de plus en plus de difficultés pour comprendre et écrire les preuves mathématiques déductives.Pour aborder ce problème, plusieurs travaux en didactique des mathématiques utilisent l’apprentissage collaboratif en classe.L'apprentissage collaboratif consiste à regrouper des étudiants pour travailler ensemble dans le but d'atteindre un objectif commun. Il repose sur le débat et l'argumentation. Les étudiants s'engagent dans des discussions pour exprimer leurs points de vue sous forme d'arguments et de contre-arguments dans le but de résoudre un problème posé.L’argumentation utilisée dans ces approches est basée sur des discussions informelles qui permettent aux étudiants d'exprimer publiquement leurs déclarations et de les justifier pour construire des preuves déductives. Ces travaux ont montré que l’argumentation est une méthode efficace pour l’apprentissage des preuves mathématiques : (i) elle améliore la pensée critique et les compétences métacognitives telles que l'auto-surveillance et l'auto-évaluation (ii) augmente la motivation des étudiants par les interactions sociales et (iii) favorise l'apprentissage entre les étudiants. Du point de vuedes enseignants, certaines difficultés surgissent avec ces approches pour l'évaluation des preuves déductives. En particulier, l'évaluation des résultats, qui comprend non seulement la preuve finale mais aussi les étapes intermédiaires, les discussions, les conflits qui peuvent exister entre les étudiants durant le débat. En effet, cette évaluation introduit une charge de travail importante pour les enseignants.Dans cette thèse, nous proposons un système pour la construction et l'évaluation des preuves mathématiques déductives. Ce système a un double objectif : (i) permettre aux étudiants de construire des preuves mathématiques déductives à partir un débat argumentatif structuré (ii) aider les enseignants à évaluer ces preuves et toutes les étapes intermédiaires afin d'identifier les erreurs et les lacunes et de fournir un retour constructif aux étudiants.Le système offre aux étudiants un cadre structuré pour débattre durant la construction de la preuve en utilisant les cadres d'argumentation proposés en intelligente artificielle. Ces cadres d’argumentation sont utilisés aussi dans l’analyse du débat qui servira pour représenter le résultat sous différentes formes afin de faciliter l’évaluation aux enseignants. Dans un second temps, nous avons implanté et validé le système par une étude expérimentale pour évaluer son acceptabilité dans la construction collaborative des preuves déductives par les étudiants et dans l’évaluation de ces preuves par les enseignants. / Learning deductive proofs is fundamental for mathematics education. Yet, many students have difficulties to understand and write deductive mathematical proofs which has severe consequences for problem solving as highlighted by several studies. According to the recent study of TIMSS (Trends in International Mathematics and Science Study), the level of students in mathematics is falling. students have difficulties to understand mathematics and more precisely to build and structure mathematical proofs.To tackle this problem, several approaches in mathematical didactics have used a social approach in classrooms where students are engaged in a debate and use argumentation in order to build proofs.The term "argumentation" in this context refers to the use of informal discussions in classrooms to allow students to publicly express claims and justify them to build proofs for a given problem. The underlying hypotheses are that argumentation: (i) enhances critical thinking and meta-cognitive skills such as self monitoring and self assessment; (ii) increases student's motivation by social interactions; and (iii) allows learning among students. From instructors' point of view, some difficulties arise with these approaches for assessment. In fact, the evaluation of outcomes -- that includes not only the final proof but also all intermediary steps and aborted attempts -- introduces an important work overhead.In this thesis, we propose a system for constructing and evaluating deductive mathematical proofs. The system has a twofold objective: (i) allow students to build deductive mathematical proofs using structured argumentative debate; (ii) help the instructors to evaluate these proofs and assess all intermediary steps in order to identify misconceptions and provide a constructive feedback to students. The system provides students with a structured framework to debate during construction of proofs using the proposed argumentation frameworks in artificial intelligence. These argumentation frameworks are also used in the analysis of the debate which will be used to represent the result in different forms in order to facilitate the evaluation to the instructors. The system has been implemented and evaluated experimentally by students in the construction of deductive proofs and instructors in the evaluation of these proofs.

Document polyvalent, la thèse a pour ambition de démontrer que le détail juridique que la facture constitue en apparence, peut masquer des problématiques épineuses. La facture a été victime d'un détournement de fonction en raison de la pratique courante de l'insertion de données qui ne figureraient pas sur une facture rudimentaire. Il y a eu une inflation de la charge juridique contenue dans le document. C'est la possibilité du « phénomène contentieux » autour de l'acceptation d'une clause insérée dans la facture qui a permis à cette dernière d'intégrer la sphère contractuelle. Ce mouvement inflationniste s'est doublé d'une appropriation étatique du document. La juridicité du document a été renforcée par le législateur au nom d'un renforcement des conditions de libre concurrence conférant alors au document une dimension technique. Le document est alors marqué du sceau de l'autonomie, celle-ci menaçant alors d'autres droits fondamentaux et notamment, le principe de légalité, au nom d'une transparence invasive. La facture est alors sans aucun doute alors une image double. Ce qui saisit, c'est la trajectoire vécue par un document plus que polyvalent ayant pour point de départ une pratique naturelle et parvenant à un point d'arrivée technique et pesant. Le droit de la facture traduit fidèlement l'état d'un droit sous tension en ce que la législation obligatoire sur la facture est contraignante et ne répond pas aux exigences de sécurité juridique. / Versatile paper, the thesis aims to demonstrate that the legal detail that the bill is apparently can hide thorny issues. The bill was the victim of a function of diversion due to the common practice of inserting data that do not appear on a rudimentary bill. There was an inflation of legal charge contained in the document. It is the possibility of " disputes phenomenon " around the acceptance of a clause in the bill which allowed the latter to integrate the contractual sphere. However, this movement is accompanied by another paradigm shift, when the legislature wished to seize the invoice into a competitive tool. Juridicity document has been strengthened by the legislature in the name of strengthening the conditions of free competition while giving the document a technical dimension. The document is then marked with the seal of autonomy, it then threatening other human rights, including the principle of legality, on behalf of invasive transparency. The invoice is then undoubtedly be a double image. What grabs is the trajectory experienced by a paper more versatile than having to base a natural practice and achieving a technical point of arrival and weighing. The right of the bill accurately reflects the state of a power law in that mandatory legislation on the invoice is binding and does not meet the requirements of legal certainty .

Le contentieux prud'homal est le point d'entrée le plus significatif pour observer la réception judiciaire de la preuve électronique. Le pragmatisme et la lexibilité de la juridiction prud'homale offre un terrain d'étude propice à la confrontation axiologique des TIC et du droit du travail et à l'étude pratique des conséquences de l'insertion d'une telle preuve dans l'argumentation des plaideurs. La présente étude s’attache à démontrer qu’à l’invocation d’une preuve électronique, lejuge du contrat de travail offre une réponse mitigée. Il adopte en effet, un comportement paradoxal : d’un côté ; il fait preuve d’audace et prend part à la reconnaissance de la preuve électronique lors de la phase d’administration de la preuve, d’un autre côté, il adopte une position de défiance et la rendinopérante. Le bilan de la recherche est proche de la désillusion : le crédit alloué à la preuve électronique n’est pas à la hauteur de son utilité processuelle, elle mérite une approche plus ambitieuse et doit faire l’objet d’une réflexion générale et approfondie. / Procedure in labour contentious matters is the most significant place to observe the judicial reception of e-proof. Pragmatism and flexibility of the elected industrial tribunal offers a field of study which is suitable to observe the axiological confrontation between ICT and labour law and to observe the practicalconsequences of the inclusion of such proof in the litigants’ argumentation. This research endeavours to demonstrate that the use of e-proof receives a mixed appreciation from the Judge of the contract of employment. Indeed, he adopts a paradoxical behaviour: on the one hand, he shows boldness and takes part in the recognition of the e-proof during the phase of producing evidence; but on the other hand, he seems to be reluctant to make use of it in an effective manner. The result of this study is disappointing when considering the credibility given to e-proof is not equal to its procedural utility; it deserves to be the subjectof a more ambitious approach and of a general and more in-depth reflexion.

Dans cette thèse, je propose trois contributions principales : dans notre première contribution, nous étudions l'architecture d'identité WebRTC et plus particulièrement son intégration aux algorithmes de délégation d'authentification existants. Cette intégration n'a pas encore été étudiée jusqu'à présent. Dans cette perspective, nous implémentons les composants de l'architecture d'identité WebRTC ce qui nous permet de montrer que cette architecture n'est pas particulièrement adaptée à une intégration aux protocoles de délégation d'authentification existants tels qu'OpenID Connect. Pour répondre à RQ1, nous montrons ensuite comment la position centrale des fournisseurs d'identité dans l'écosystème du Web est renforcée par leur intégration à l'établissement de session WebRTC, posant ainsi un risque supplémentaire contre la discrétion des utilisateurs. Dans l'écosystème Web, la norme est l'architecture des services en silo dont les utilisateurs sont captifs. C'est en particulier le cas des systèmes de délégation d'authentification, pour lesquels la plupart du temps, il n'est pas possible de choisir son fournisseur d'identité. Afin de répondre à RQ3, nous réalisons une étude afin de déterminer pour quelles raisons les utilisateurs ne peuvent pas choisir leur fournisseur d'identité sur Web. Notre étude montre que bien que ce choix soit possible en théorie, l'absence d'implémentation de certains standards par les sites webs et les fournisseurs d'identité empêche ce choix en pratique. Dans notre seconde contribution, nous cherchons à donner plus de contrôle à l'utilisateur. Pour ce faire et en réponse à RQ2, nous proposons une extension de la spécification WebRTC afin de permettre la négociation des paramètres d'identité. Un prototype d'implémentation est proposé afin de valider notre proposition. Cette implémentation révèle certaines limites dues à l'API d'identité WebRTC empêchant notamment d'obtenir un retour sur le niveau d'authentification de l'autre utilisateur ainsi que l'impossibilité de changer de fournisseur d'identité en cours de session. Nous proposons ensuite une API Web permettant aux utilisateurs de choisir leur fournisseur d'identité lors d'une authentification sur un site tiers via une interface de sélection d'identité contrôlée par le navigateur. Répondant à RQ3, notre API repose sur une réutilisation de l'architecture d'identité WebRTC dans un scénario client-serveur. Nous présentons une implémentation de notre solution, basée sur une extension du navigateur Firefox, afin d'en démontrer l'utilisabilité. Nos résultats montrent qu'à long terme, l'adoption de cette API pourrait réduire la charge d'implémentation pour les développeurs de sites Web et permettre aux utilisateurs de préserver leur discrétion en choisissant des fournisseurs d'identité de confiance. / In this thesis, we propose three main contributions : In our first contribution we study the WebRTC identity architecture and more particularly its integration with existing authentication delegation protocols. This integration has not been studied yet. To fill this gap, we implement components of the WebRTC identity architecture and comment on the issues encountered in the process. In order to answer RQ1, we then study this specification from a privacy perspective an identify new privacy considerations related to the central position of identity provider. In the Web, the norm is the silo architecture of which users are captive. This is even more true of authentication delegation systems where most of the time it is not possible to freely choose an identity provider. In order to answer RQ3, we conduct a survey on the top 500 websites according to Alexa.com to identify the reasons why can't users choose their identity provider. Our results show that while the choice of an identity provider is possible in theory, the lack of implementation of existing standards by websites and identity providers prevent users to make this choice. In our second contribution, we aim at giving more control to users. To this end and in order to answer RQ2, we extend the WebRTC specification to allow identity parameters negotiation. We present a prototype implementation of our proposition to validate it. It reveals some limits due to the WebRTC API, in particular preventing to get feedback on the other peer's authentication strength. We then propose a web API allowing users to choose their identity provider in order to authenticate on a third-party website, answering RQ2. Our API reuse components of the WebRTC identity architecture in a client-server authentication scenario. Again, we validate our proposition by presenting a prototype implementation of our API based on a Firefox extension. Finally, in our third contribution, we look back on RQ1 and propose a trust and security model of a WebRTC session. Our proposed model integrates in a single metric the security parameters used in the session establishment, the encryption parameters for the media streams, and trust in actors of the communication setup as defined by the user. Our model objective is to help non-expert users to better understand the security of their WebRTC session. To validate our approach, we conduct a preliminary study on the comprehension of our model by non-expert users. This study is based on a web survey offering users to interact with a dynamic implementation of our model.

No description available.

La raison initiale du sujet de cette thèse est l'introduction, pour la première fois en France, d'éléments de théorie des graphes dans un curriculum de l'enseignement secondaire, à savoir celui de la spécialité mathématiques de la Terminale économique et sociale (ES) en 2002.<br />Après une brève étude historique de la genèse – relativement récente – du graphe en tant que concept mathématique et de la signification épistémologique de cette genèse, nous analysons les choix faits pour la transposition de ce concept, en particulier les énoncés proposés aux élèves, qui montrent le décalage entre les intentions affichées et la réalité. Cette partie du programme de terminale ES se particularise par sa mise en œuvre « axée sur le seule résolution de problèmes ».<br />Or, nous montrons que les manuels scolaires sont dans ce chapitre composés d'exercices et non de problèmes. L'enseignement de théorie des graphes, s'il se limite à la résolution, locale, de ces exercices ou de « casse-tête » mathématiques, ne permet pas aux élèves de comprendre les concepts mathématiques sous-jacents ni surtout d'accéder au sens du raisonnement mathématique (en particulier autour de la modélisation et de la preuve) et à la richesse de la démarche scientifique, ce qu'aurait dû permettre ce domaine facilement abordable des mathématiques.<br />Une étude théorique et expérimentale du problème de « parcours eulériens dans les graphes » a ensuite été menée, du primaire au supérieur, sous des formes différentes (situations-recherche en classe avec ou sans support matériel, étude de documents). Des éléments didactiques ont aussi été tirés de deux stages de formation d'enseignants en théorie des graphes pour la Terminale ES.<br />Ces différentes études nous ont conduit à proposer un nouvel ensemble organisé de problèmes à destination des enseignants de Terminale ES, accompagnés de leur résolution et d'analyses didactiques qui attestent que des mathématiques plus consistantes peuvent être abordées et construites sur ce thème.

L'étude réalisée montre un décalage important entre la preuve en mathématiques et la preuve telle qu'elle vit en classe, surtout au collège : actuellement la transposition didactique dénature son sens, réduisant son apprentissage à celui de savoir faire des exercices d'écriture formelle. Il s'avère nécessaire de changer les pratiques, pour que la preuve soit enseignée de manière plus satisfaisante sur les plans épistémologique et didactique. Nous montrons qu'il est pertinent, et possible, d'amorcer ce changement par un travail sur les conceptions des enseignants. Pour cela nous proposons une ingénierie de formation fondée sur trois problèmes : tout d'abord est montré le rapport existant des élèves à la preuve ; ensuite, les enseignants, mis en situation de recherche de problèmes, produisent des preuves. Les résultats obtenus à partir des problèmes choisis permettent à la fois de préciser le rapport des enseignants à la preuve et d'amorcer avec eux une réflexion sur leurs pratiques.

Les substitutions explicites ont été introduites comme un raffinement du lambda-calcul, celui-ci étant le<br />formalisme utilisé pour étudier la sémantique des langages de programmation. L'objet de cette thèse<br />est l'étude de leurs propriétés de normalisation forte et de préservation de la normalisation forte. Ce<br />manuscrit rend compte de plusieurs travaux autour de ces propriétés de normalisation, regroupés en<br />trois volets.<br /><br />Le premier d'entre eux formalise une technique générale de preuve de normalisation forte utilisant<br />la préservation de la normalisation forte. On applique cette technique à un spectre assez large de calculs<br />avec substitutions explicites afin de mesurer les limites de son utilisation. Grâce à cette technique, on<br />prouve un résultat nouveau : la normalisation forte du lambda-upsilon-calcul simplement typé.<br /><br />Le deuxième travail est l'étude de la normalisation d'un calcul symétrique non-déterministe issu de<br />la logique classique formulée dans le calcul des séquents, auquel est ajouté des substitutions explicites.<br />La conjonction des problèmes posés par les calculs symétriques et ceux posés par les substitutions<br />explicites semble vouer à l'échec l'utilisation de preuves par réductibilité. On utilise alors la technique<br />formalisée dans le premier travail, ce qui nous demande de prouver tout d'abord la préservation de la<br />normalisation forte. A cette fin, on utilise un fragment de la théorie de la perpétuité dans les systèmes<br />de réécriture.<br /><br />La définition d'une nouvelle version du lambda-ws-calcul avec nom, le lambda-wsn-calcul, constitue le troisième<br />volet de la thèse. Pour prouver sa normalisation forte par traduction et simulation dans les réseaux<br />de preuve, on enrichit l'élimination des coupures de ceux-ci avec une nouvelle règle, ce qui nous oblige<br />à prouver que cette nouvelle notion de réduction est fortement normalisante.

Après un historique bref et général de la déduction automatique, on analyse les tendances actuelles et les besoins en présentation de preuves et communication d'outils d'inférence. Les notions théoriques concernées sont présentées et étudiées en détail. On donne ensuite une synthèse comparative critique et exhaustive de l'état de l'art. Cette synthèse manquait dans la littérature. L'analyse des notions fondamentales en logique et la synthèse sur l'état de l'art permettent d'établir les caractéristiques retenues pour le système GLEF (Graphical & Logical Edition Framework). La conception et la réalisation de deux langages ont permis de rendre GLEF générique (c'est à dire paramétrable par le système formel employé et par la présentation de ses preuves). Un formalisme de définition, fondé sur le Calcul des Construction (dû à Coquand et Huet), sert à représenter et à vérifier les systèmes formels et les preuves dans ses systèmes formels. Un langage de présentation, fondé sur la notion de «boîte», sert à décrire leur présentation. En annexe nous donnons un algorithme original pour l'opération d'effacement, particulièrement difficile en lambda-calcul typé, qui sert à réaliser la commande «couper» de GLEF. GLEF a été développé au sein du projet ATINF (ATelier d'INFérence). Un manuel utilisateur rudimentaire et de nombreux exemples d'utilisation en sont donnés. Certains exemples montrent comment, après avoir spécifié la définition et la présentation d'un système formel objet, un utilisateur de GLEF peut construire ou visualiser des preuves en manipulant directement les objets (formules, preuves partielles, etc.) à l'écran, avec la souris. D'autres illustrent comment GLEF présente les preuves produites par les démonstrateurs d'ATINF ou extérieurs à ATINF. Les principales lignes de recherche future concluent ce travail

.