Les TICE pour la production écrite et la traduction de l'italien vers le français : le cas de la SSLMIT de Forlì

Les recherches relatives à l'utilisation des TICE se concentrent fréquemment soit sur la dimension cognitive, sur la dimension linguistique ou sur la dimension culturelle. Le plus souvent, les recherches empiriques se proposent d'évaluer les effets directs des TICE sur les performances langagières des apprenants. En outre, les recherches, surtout en psychologie cognitive, sont le plus souvent effectuées en laboratoire. C'est pourquoi le travail présenté dans cette thèse se propose d'inscrire l'utilisation des TICE dans une perspective écologique, et de proposer une approche intégrée pour l'analyse des pratiques effectives aussi bien en didactique des langues qu'en didactique de la traduction. En ce qui concerne les aspects cognitifs, nous recourons à un concept apprécié des praticiens, celui de stratégies d'apprentissage. Les quatre premiers chapitres de la présente thèse sont consacrés à l'élaboration du cadre théorique dans lequel nous inscrivons notre recherche. Nous aborderons en premier lieu les aspects disciplinaires, et notamment l’interdisciplinarité de nos deux champs de référence. Ensuite nous traiterons les stratégies d'apprentissage et les stratégies de traduction. Dans un troisième mouvement, nous nous efforcerons de définir les deux compétences visées par notre recherche : la production écrite et la traduction. Dans un quatrième temps, nous nous intéresserons aux modifications introduites par les TICE dans les pratiques d'enseignement et d'apprentissage de ces deux compétences. Le cinquième chapitre a pour objet la présentation, l'analyse des données recueillies auprès de groupes d'enseignants et d'étudiants de la section de français de la SSLMIT. Il s’agira dans un premier temps, de présenter notre corpus. Ensuite nous procéderons à l’analyse des données. Enfin, nous présenterons, après une synthèse globale, des pistes didactiques et scientifiques à même de prolonger notre travail.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.