Thesis (M.S.)--Marquette University, 2009. / Douglas Harris, Sheikh Iqbal Ahamed, Praveen Madiraju, Advisors.

K.E. IVERSON a défini le langage APL en 1962 dans un ouvrage intitulé "A Progrannning Language". Malgré les difficultés nouvelles que posait ce langage aux implémenteurs, des interprètes APL furent rapidement disponibles chez IBM, d'abord à titre expérimental, en 1965, puis commercialisés sur ordinateur 1130 et 360 (A3, A4). En effet, ce langage s.'était d'emblée révélé intéressant pour toutes les applications réclamant plus de programmation que de longs calculs. Depuis cette époque, d'autres interprètes APL ont vu le jour chez d'autres constructeurs (B2, B3, B4, B8). Cependant, réalisés sur de gros ordinateurs, ils réclament des ressources hors de proportion avec les moyens habituels des ingénieurs ou des étudiants. Dans cette optique, il a paru intéressant de réaliser un interprète APL sur une petite machine, partagée entre plusieurs utilisateurs.

Thesis (Ph. D.)--University of Washington, 2001. / Vita. Includes bibliographical references (p. 104-113).

Thesis (M.S.)--University of California, Santa Cruz, 1993. / Typescript. Includes bibliographical references (leaves 183-189).

Orientador: Wilson Massashiro Yonezawa / Banca: Nelson Antonio Pirola / Banca: Elaine Pasqualini / Resumo: O baixo desempenho em matemática obtido pelos alunos brasileiros nas avaliações externas revela que o ensino da matemática é um grande desafio tanto para as nações marcadas pela desigualdade social, quanto para as nações mais desenvolvidas. Em busca da superação dos baixos índices de rendimento dos estudantes em matemática, este trabalho de cunho qualitativo, investigou por meio da aprendizagem situada numa comunidade de prática de programadores as formas pelas quais os alunos com baixo desempenho em matemática se relacionam com a mesma durante e após participarem de oficinas de programação. A pesquisa contou com oito oficinas de programação utilizando a ferramenta Processing 2. Foi possível delinear seis categorias de análise que, conforme os objetivos da pesquisa, sinalizam arranjos da aprendizagem situada da matemática numa comunidade de prática de programadores - não linearidade, ênfase no saber fazer, informal, construção do conhecimento a partir da necessidade, interatividade e engajamento e tentou-se buscar subsídios para responder perguntas como: Quais são as vantagens de aulas de matemática utilizando ferramentas de programação? Quais são as dificuldades ao desenvolver aulas de matemática utilizando ambiente de programação? Que tipos de mudança o uso de ferramentas de programação provocam na dinâmica das aulas de matemática? Para a realização da pesquisa foi escolhida uma escola da rede municipal de ensino fundamental do município de Santa Cruz do Rio Pardo - SP, com seis alunos, na faixa etária de 12 anos que apresentavam baixo rendimento na disciplina. A programação de computadores como instrumento didático-pedagógico, no emprego da ferramenta Processing 2 aponta avanços na aprendizagem dos alunos, no tocante a promoção de um trabalho mais cooperativo, que coloca o erro como elemento natural no processo de aprendizagem, e tona a aprendizagem mais interativa, contribuindo para um... / Abstract: The poor performance in mathematics obtained by Brazilian students in the external evaluation shows that mathematics teaching is a major challenge for both nations market by social inequality, and for the most developed nations. In search of overcoming low levels of student performance in mathematics, the qualitative nature of work, investigated through learning located in a developer community of practice the ways in which students with low math performance relate to the same during and after participating in scheduling workshops. The research included eight workshops programming using Processing tool 2. It was possible to outline six categories of analysis that, as the research objectives, signal arrangements situated learning of mathematics in a a developer community of practice - nonlinearity, emphasis on know-how, informal, knowledge building from the need, interactivity and engagement and we tried to get subsidies to answer questions such as: What are the advantages of math classes using programming tools? What are the difficulties in developing math classes using programming environment? What kinds of changes using programming tools cause the dynamics of math classes? For the research was chosen a school elementary school municipal system of the city of Santa Cruz do Rio Pardo - SP, with six students, aged 12 who had low performance in the discipline. The programming computers as didactic and pedagogical tool, the use of Processing 2 tool shows progress in student learning, regarding the promotion of a more cooperative work, which puts the error as a natural element in the learning more interactive, contribuing to an immediate feedback, and advancing above all in the ownership of adjancent mathematical concepts of programming activity. In became clear that in the course of the workshops students have come to realize the need and importance of mathematics as they build programs that represent their wishes and desires. Thus the... / Mestre

Mes travaux de recherche portent sur les modèles de programmation distribuée, principalement par objets et composants. Dans ce domaine, j'ai travaillé à fournir des outils facilitant la programmation d'applications distribuées à large échelle et vérifiant la correction de leur comportement. Pour faciliter la programmation d'applications distribuées je me suis intéressé à la mise au point de langages avec un fort niveau d'abstraction: objets actifs, squelettes algorithmiques, composants. Afin de vérifier la correction du comportement d'une application j'ai collaboré à la mise au point d'outils de spécification et de vérification comportementales d'applications distribuées. Mes travaux ont pour but de fournir un modèle formel des langages de programmations, des bibliothèques, et des environnements d'exécution fournies au programmeur afin de garantir un comportement sûr des applications distribuées. Ma thèse m'a permis de mettre au point le calcul ASP modélisant lecomportement des objets actifs et des futurs. Depuis, nous avons créé une version fonctionnelle de ce calcul que nous avons modélisé en Isabelle/HOL. Aussi j'ai fortement contribué à la définition d'un modèle à composants distribués -- le GCM (Grid Component model)--, à sa formalisation et à son utilisation pour programmer des composants adaptables ou autonomes. Enfin, j'ai contribué à la spécification et la vérification comportementale des programmes utilisant des objets actifs et des composants afin de garantir la sûreté de leur exécution. Actuellement, nous travaillons à la fois à une extension multi-threadée du modèle à objets actifs mieux adaptée aux machines multi-coeurs, et à l'utilisation de méthodes formelles pour mettre au point et prouver la correction d'un algorithme de diffusion pour réseau pair-à-pair de type CAN (Content Adressable Network). Ce manuscrit fournit une vue d'ensemble de tous ces travaux.

Mes travaux s'articulent principalement autour de trois axes concernant la programmation sécurisée, plus particulièrement dans le cadre d'applications distribuées. Ainsi, nous considérons plusieurs participants ne se faisant pas mutuellement confiance et ayant des niveaux de sécurité différents. On s'intéresse alors au garanties restantes lorsque certains de ces participants sont compromis. Par exemple, lors d'une opération de commerce électronique, le client, le serveur, et la banque ne se font pas mutuellement confiance et font encore moins confiance aux machines intermédiaires du réseau; on veut pourtant qu'une transaction sécurisée puisse avoir lieu.

Ce manuscrit de thèse présente les travaux menés sur le système de modules de l'assistant de Preuve Coq.

Le but de cet thèse est de contribuer à rendre la programmation Web plus flexible et plus sûre qu'elle ne l'est avec les solutions répandues actuellement. Pour ceci, nous proposons une solution dans la lignée de la famille de langages ML, qui laisse un maximum de liberté au programmeur de part son côté multi-paradigmes, tout en offrant un degré de sûreté important grâce au typage statique. Dans une première partie, nous montrons qu'il est possible de programmer le navigateur sans se plier au style de JavaScript. Notre solution est OBrowser, une implantation en JavaScript de la machine virtuelle OCaml. L'implantation prend en charge l'ensemble du langage OCaml et de sa bibliothèque, y compris le modèle de concurrence préemptif. Nous présentons de plus un mécanisme d'inter-opérabilité entre les couches objet de JavaScript et d'OCaml, permettant d'utiliser de façon bien typée l'environnement du navigateur avec les objets d'OCaml. Dans une seconde partie, nous fournissons une API de manipulation du document plus sûre et de plus haut niveau que le DOM des navigateurs. En particulier, nous cherchons à éliminer les déplacements implicites effectués par le DOM pour maintenir la forme d'arbre, qui limitent les possibilités de typage statique. Nous donnons d'abord fDOM, un modèle formel minimal similaire au DOM. Puis nous proposons cDOM, un modèle alternatif ou les déplacements sont remplacés par des copies. Nous décrivons ensuite FidoML, un langage basé sur ML, permettant les manipulations bien typées du document grâce à l'utilisation de cDOM. Dans toute cette partie, nous faisons attention à ce que les solutions données soient aussi adaptables que possible. Dans une troisième partie, nous montrons comment les travaux, jusqu'ici principalement pré- sentés dans le cadre du navigateur, s'appliquent à un contexte multi-tiers. Nous donnons d'abord un tour d'horizon des plates-formes multi-tiers proches issues de la recherche. Nous décrivons en particulier les solutions qu'elles apportent à un ensemble de problématiques spécifiques à la pro- grammation Web. Puis nous concluons en présentant les grandes lignes d'un langage multi-tiers mettant à profit les travaux des deux premières parties dans les solutions à ces différentes problé- matiques.

Les systèmes basés sur la Théorie des Types prennent une importance considérable tant pour la vérification de programmes qu'en tant qu'outils permettant la preuve formelle de théorèmes mettant en jeu des calculs complexes. Ces systèmes nécessitent aujourd'hui une grande expertise pour être utilisés efficacement. Nous développons des constructions de haut niveau permettant d'utiliser les langages basés sur les théories des types dépendants aussi simplement que les langages de programmation fonctionnels usuels, sans sacrifier pour autant la richesse des constructions disponibles dans les premiers. Nous étudions un nouveau langage permettant l'écriture de programmes certifiés en ne donnant que leur squelette algorithmique et leur spécification. Le typage dans ce système donne lieu à la génération automatique d'obligations de preuve pouvant être résolues a posteriori. Nous démontrons les propriétés métathéoriques essentielles du système, dont les preuves sont partiellement mécanisées, et détaillons son implémentation dans l'assistant de preuve Coq. D'autre part, nous décrivons l'intégration et l'extension d'un système de "Type Classes" venu d'Haskell à Coq via une simple interprétation des constructions liées aux classes dans la théorie des types sous-jacente. Nous démontrons l'utilité des classes de types dépendantes pour la spécification et la preuve et présentons une implémentation économique et puissante d'une tactique de réécriture généralisée basée sur les classes. Nous concluons par la mise en œuvre de l'ensemble de ces contributions lors du développement d'une bibliothèque certifiée de manipulation d'une structure de données complexe, les "Finger Trees".