Nous nous intéressons ici à la génération de programmes certifiés<br />corrects par construction. Ces programmes sont obtenus en<br />extrayant l'information pertinente de preuves constructives réalisées<br />dans l'assistant de preuves Coq.<br /><br />Une telle traduction, ou "extraction", des preuves constructives<br />en programmes fonctionnels n'est pas nouvelle, elle correspond <br />à un isomorphisme bien connu sous le nom de Curry-Howard. Et<br />l'assistant Coq comporte depuis longtemps un tel outil d'extraction. <br />Mais l'outil précédent présentait d'importantes limitations. Certaines <br />preuves Coq étaient ainsi hors de son champ d'application, alors que <br />d'autres engendraient des programmes incorrects.<br /><br />Afin de résoudre ces limitations, nous avons effectué une refonte<br />complète de l'extraction dans Coq, tant du point de vue de la théorie<br />que de l'implantation. Au niveau théorique, cette refonte a entraîné<br />la réalisation de nouvelles preuves de correction de ce mécanisme<br />d'extraction, preuves à la fois complexes et originales. Concernant<br />l'implantation, nous nous sommes efforcés d'engendrer du code <br />extrait efficace et réaliste, pouvant en particulier être intégré dans des<br />développement logiciels de plus grande échelle, par le biais de<br />modules et d'interfaces.<br /><br />Enfin, nous présentons également plusieurs études de cas illustrant<br />les possibilités de notre nouvelle extraction. Nous décrivons ainsi la<br />certification d'une bibliothèque modulaire d'ensembles finis, et <br />l'obtention de programmes d'arithmétique réelle exacte à partir d'une <br />formalisation d'analyse réelle constructive. Même si des progrès <br />restent encore à obtenir, surtout dans ce dernier cas, ces exemples <br />mettent en évidence le chemin déjà parcouru.

Cette thèse traite principalement des contreparties combinatoires et constructives de certains théorèmes d'optimisation combinatoire qui font appel à des outils de topologie algébrique. Des généralisations des lemmes de Sperner et des formules combinatoires de Ky Fan sont proposées, ainsi que des applications à la coloration des graphes de Kneser et au célèbre problème du partage équitable du collier. Un problème d'ordonnancement lié à ce dernier problème est également abordé. Enfin, le dernier chapitre contient des résultats nouveaux pour les sigma-jeux (jeux de lampes) sur la grille.

Le logiciel Coq est un assistant à la preuve basé sur le Calcul des<br />Constructions Inductives.<br /> Dans cette thèse nous proposons d'améliorer l'automatisation de ce<br /> système en le dotant d'une procédure de décision réflexive et complète<br />pour la théorie du premier ordre de l'arithmétique réelle.<br /> La théorie des types implémentée par le système Coq comprend un<br />langage fonctionnel typé dans lequel nous avons programmé un<br />algorithme de Décomposition Algébrique Cylindrique (CAD). Cet<br />algorithme calcule une partition de l'espace en cellules<br />semi-algébriques sur lesquelles tous les polynômes d'une famille donnée <br />ont un signe constant et permet ainsi de décider les formules de cette théorie.<br /> Il s'agit ensuite de prouver la correction de l'algorithme et de la<br />procédure de décision associée avec l'assistant à la preuve Coq.<br /> Ce travail comprend en particulier une librairie d'arithmétique polynomiale<br />certifiée et une partie significative de la preuve formelle de correction de<br />l'algorithme des sous-résultants. Ce dernier algorithme permet de calculer<br />efficacement le plus grand commun diviseur de polynômes à coefficients dans un<br />anneau, en particulier à plusieurs variables.<br /> Nous proposons également une tactique réflexive de décision des égalités dans les<br />structures d'anneau et de semi-anneaux qui améliore les performances de l'outil<br />déjà disponible et augmente son spectre d'action en exploitant les possibilités de<br />calcul du système.<br /> Dans une dernière partie, nous étudions le contenu calculatoire d'une preuve<br />constructive d'un lemme élémentaire d'analyse réelle, le principe d'induction<br />ouverte.

Cette thèse porte sur l'adaptation de la réalisabilité et la paramétricité au cas des types dépendants dans le cadre des Systèmes de Types Purs. Nous décrivons une méthode systématique pour construire une logique à partir d'un langage de programmation, tous deux décrits comme des systèmes de types purs. Cette logique fournit des formules pour exprimer des propriétés des programmes et elle offre un cadre formel adéquat pour développer une théorie de la réalisabilité au sein de laquelle les réalisateurs des formules sont exactement les programmes du langage de départ. Notre cadre permet alors de considérer les théorèmes de représentation pour le système T de Gödel et le système F de Girard comme deux instances d'un théorème plus général.Puis, nous expliquons comment les relations logiques de la théorie de la paramétricité peuvent s'exprimer en terme de réalisabilité, ce qui montre que la logique engendrée fournit un cadre adéquat pour développer une théorie de la paramétricité du langage de départ. Pour finir, nous montrons comment cette théorie de la paramétricité peut-être adaptée au système sous-jacent à l'assistant de preuve Coq et nous donnons un exemple d'application original de la paramétricité à la formalisation des mathématiques.

Dans ce mémoire, nous nous interrogeons sur de nouvelles règles de preuve du Code criminel pour déterminer si elles ont complètement éliminé le phénomène de victimisation des plaignantes dans les procédures en matière d'agression sexuelle. Nous émettons l'hypothèse qu'elles n'ont pas éliminé le traitement inéquitable des victimes dans le procès pénal et que ce traitement inéquitable nuit autant à la recherche de la vérité qu'au respect des droits des plaignantes. Nous examinons d'abord les droits constitutionnels respectifs de la plaignante et de l'accusé dans le procès en matière de crimes sexuels et leur interaction avec des règles qui portent sur la réputation et l'état de santé des deux protagonistes dans de telles affaires. Nous observons que ces règles de preuve offriraient une symétrie apparente au sujet du traitement de la mauvaise réputation de l'accusé et de la réputation sexuelle et la santé mentale de la victime dans la procédure. Cette symétrie serait toutefois imparfaite, inappropriée ou biaisée par le caractère adversaire du procès et la priorité accordée aux droits constitutionnels de l'inculpé et ce, parfois même au détriment de la vérité et de la justice. Enfin, nous proposons des modifications aux règles actuelles de preuve et de procédure en matière d'agression sexuelle pour favoriser une meilleure recherche de la vérité et un respect accru des droits constitutionnels des victimes / In this master's thesis, we will ask whether the new rules of evidence in the Criminal Code have eliminated the phenomenon of victimization of complainants in sexual assault matters. We emit the hypothesis that the new rules of evidence have not eliminated the inequitable treatment of female plaintiffs in criminal trials and that this inequitable treatment is equally harmful to the search for the truth as well as to the respect of the victim's rights. First, we will state the constitutional rights of the plaintiff and of the accused party in matters of sexual crimes and the current rules of evidence specifically in regards to the reputation and the state of health of the two parties, the accused and the plaintiff, in sexual assault trials and in regards to their respective constitutional rights in such matters. In particular, we will examine the existence of a noticeable symmetry between the rules of evidence relative to the bad reputation of the accused and those concerning the sexual reputation and mental health of the victim, a symmetry which is nevertheless imperfect, inappropriate or biased because of the adversarial procedure and the constitutional debate which we will examine in second place. Thirdly, we will propose certain modifications be made to the rules of evidence and procedure in matters of sexual assault to encourage the discovery of the truth and the respect of the plaintiff’s constitutional rights.

Les technologies de l’information entraînent de profondes transformations dans nos façons d’apprendre et de socialiser ; de lire et d’écrire. Ces changements ne sont pas sans conséquence sur de nombreuses institutions, juridiques ou non. Créées au fil du temps et adaptées à une réalité qu’elles avaient internalisée, elles doivent aujourd’hui comprendre et s’adapter au changement. L’écrit est une de ces institutions. Sa place dans le droit civil est le fruit de centaines d’années de cohabitation et le droit y a vu un allié stable. Mais autrefois facilitateur, l’écrit devient obstacle alors que les technologies de l’information, affranchies du papier, sont utilisées dans des situations juridiques. Comment adapter la notion d’écrit – et celles de l’original et de la signature – alors qu’il n’est question que de données abstraites sous forme numérique ? C’est là l’objet de ce mémoire. Suite à une étude de la notion d’écrit dans le temps, de son affirmation à son bouleversement, nous étudierons les outils juridiques (traditionnels ou récents, comme les principes de neutralité technologique et d’équivalence fonctionnelle) à la disposition du droit civil pour constamment s’adapter à des situations changeantes. Enfin, dans une perspective plus pratique, nous verrons le traitement qu’ont fait divers législateurs, de l’écrit électronique. Nous terminerons par une analyse plus précise des dispositions québécoises relatives à l’écrit électronique. Les principes étudiés dans ce mémoire sont susceptibles de s’appliquer à d’autres situations similaires. / Information technology has completely modified our way of learning, socialising, reading and writing. These changes have also affected numerous institutions. Developed over many years and adapted to a reality they internalised, they now have to understand the nature of the changes taking place and adapt to them. The legal concept of “writing” is such an institution. Its place in the realm of civil law is the result of hundreds of years of cohabitation. The legal system has found a great ally in “writings”. However, although “writing” has been seen as an enabler in the past, the use of information technologies in legal circumstances has turned it into an obstacle. How are we going to adapt the notion of writing – and those of original and signature – when talking about digital data ? This is the topic of our thesis. Following a historical study of the concept of “writing”, from its inception to its current state of crisis, we will analyse the legal tools made available to civil law (whether they be traditional or recent, such as the technological neutrality, and functional equivalence principles) in order to adapt to a constantly changing technological landscape. On a more practical level, we will study how different legislators have addressed electronic documents. Our study will conclude with an analysis of Quebec legislation pertaining to electronic documents. The principles studied in this thesis should be applicable to other similar situations.

Les chercheurs s’étant penchés sur les facteurs influençant la décision du suspect de confesser son crime ont mis en évidence que deux facteurs sont principalement influents : la force de la preuve (Des Lauriers-Varin et St-Yves, 2006; Moston et al., 1992) et la conduite de l’enquêteur (Holmberg et Christianson, 2002; Kebell et al., 2005). Par contre, les contradictions entre ces études ont apporté davantage de confusion que de réponses à la pratique. Cette étude vise donc à explorer l’incidence de ces deux facteurs sur l’inclination du suspect à confesser son crime et les possibles interactions entre eux. Pour ce faire, 50 enregistrements vidéo d’interrogatoires d’homicide furent visionnés et les données furent soumises à des analyses statistiques et qualitatives. Les résultats d’une régression logistique démontrent que la conduite de l’enquêteur est le facteur prédominant pour prédire l’obtention d’aveux du suspect en contrôlant pour l’effet des variables statiques et de la preuve. Également, les résultats mettent en évidence qu’en augmentant les attitudes et comportements associés à une conduite « positive », l’enquêteur augmentait les probabilités d’aveux du suspect. De plus, les résultats indiquent que l’augmentation du nombre d’éléments de preuves est associée à une plus grande démonstration de « rapport de force » de la part de l’enquêteur. Les résultats sont discutés en relation à l’effet des principaux facteurs sur les schémas et dynamiques prenant place entre l’enquêteur et le suspect. / The studiess on factors influencing a suspect’s decision to confess his crime during a police questioning, reveal that the strength of evidence (Moston et al., 1992 and Des Lauriers-Varin and St-Yves, 2006) and the detective’s behaviour (Holmberg et Christianson, 2002 et Kebell et al., 2005) are considered key factors. However, past studies show notable contradictions. The present work focuses on the role of the two aforementioned factors, in the suspect’s decision to confess a crime and the potential interaction effect among them. The data were obtained by visioning and analyzing 50 questionings of a suspect linked to a homicide investigation. The logistic regression’s results show that the detective’s behaviour is the predominant factor in obtaining a confession from a suspect. Theses results are maintained when both the characteristic of the suspect and the weight of evidence are controlled for. Moreover, our results suggest that a “positive” attitude from the detective’s part is associated with a greater propensity toward confessing. Also, the results indicate that the greater available evidence to support the case, will translate into more “dominant” style of questioning from the detectives. The results are discussed in relation to the effects of the different dynamics taking place between the detective and the suspect during the questioning.

L’un des buts de l’apprentissage des mathématiques est le développement du raisonnement et celui-ci participe à la compréhension des mathématiques. Très liée au raisonnement, la notion de preuve est aussi fondamentale à l’apprentissage des mathématiques, car elle permet d’établir la validité d’arguments mathématiques et de conférer un sens à différents concepts à travers l’explication de l’organisation logique du travail effectué. Toutefois, malgré l’importance accordée au développement de différents types de raisonnements, plusieurs élèves éprouvent des difficultés lorsqu’ils sont appelés à concevoir ou à évaluer des preuves. Dans le cadre de cette recherche, nous avons étudié l’impact de l’utilisation d’un forum électronique sur le développement d’habiletés de validation algébrique ainsi que sur le développement d’habiletés en lien avec l’évaluation de preuves en algèbre chez des élèves de 13 et 14 ans du Nouveau-Brunswick et du Québec. Les résultats laissent supposer que l’utilisation du forum électronique encourage le passage des preuves pragmatiques aux preuves intellectuelles, en plus de favoriser une utilisation adéquate des règles du débat mathématique. / One of the goals of learning mathematics is the development of reasoning, because it is essential to understand mathematics. Closely related to reasoning, the notion of proof is also fundamental in the learning of mathematics, because it allows students to establish the validity of mathematical arguments and put a sense on various concepts through logical explanation of their work. However, in spite of the importance placed on the development of the capacity to reason mathematically, several students are confronted with difficulties during the development or the evaluation of proofs. This study examined the impact of the use of a discussion forum on the development of algebraic validation skills as well as on the development of skills linked with the evaluation of the proof process in algebra with 13 and 14 year old students from New Brunswick and Quebec (Canada). The results lead us to believe that the use of the electronic forum encourages the passage from pragmatic proofs to intellectual proofs. It also seems to facilitate an adequate use of the rules of the mathematical debate.

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal