La problématique centrale de cette thèse est l'élaboration d'un opérateur de Laplace--Beltrami discret sur les surfaces digitales. Ces surfaces proviennent de la théorie de la géométrie discrète, c’est-à-dire la géométrie qui s'intéresse à des sous-ensembles des entiers relatifs. Nous nous plaçons ici dans un cadre théorique où les surfaces digitales sont le résultat d'une approximation, ou processus de discrétisation, d'une surface continue sous-jacente. Cette méthode permet à la fois de prouver des théorèmes de convergence des quantités discrètes vers les quantités continues, mais aussi, par des analyses numériques, de confirmer expérimentalement ces résultats. Pour la discrétisation de l’opérateur, nous faisons face à deux problèmes : d'un côté, notre surface n'est qu'une approximation de la surface continue sous-jacente, et de l'autre côté, l'estimation triviale de quantités géométriques sur la surface digitale ne nous apporte pas en général une bonne estimation de cette quantité. Nous possédons déjà des réponses au second problème : ces dernières années, de nombreux articles se sont attachés à développer des méthodes pour approximer certaines quantités géométriques sur les surfaces digitales (comme par exemple les normales ou bien la courbure), méthodes que nous décrirons dans cette thèse. Ces nouvelles techniques d'approximation nous permettent d'injecter des informations de mesure sur les éléments de notre surface. Nous utilisons donc l'estimation de normales pour répondre au premier problème, qui nous permet en fait d'approximer de façon précise le plan tangent en un point de la surface et, via une méthode d'intégration, palier à des problèmes topologiques liées à la surface discrète. Nous présentons un résultat théorique de convergence du nouvel opérateur discrétisé, puis nous illustrons ensuite ses propriétés à l’aide d’une analyse numérique de l’opérateur. Nous effectuons une comparaison détaillée du nouvel opérateur par rapport à ceux de la littérature adaptés sur les surfaces digitales, ce qui nous permet, au moins pour la convergence, de montrer que seul notre opérateur possède cette propriété. Nous illustrons également l’opérateur via quelques unes de ces applications comme sa décomposition spectrale ou bien encore le flot de courbure moyenne / The central issue of this thesis is the development of a discrete Laplace--Beltrami operator on digital surfaces. These surfaces come from the theory of discrete geometry, i.e. geometry that focuses on subsets of relative integers. We place ourselves here in a theoretical framework where digital surfaces are the result of an approximation, or discretization process, of an underlying smooth surface. This method makes it possible both to prove theorems of convergence of discrete quantities towards continuous quantities, but also, through numerical analyses, to experimentally confirm these results. For the discretization of the operator, we face two problems: on the one hand, our surface is only an approximation of the underlying continuous surface, and on the other hand, the trivial estimation of geometric quantities on the digital surface does not generally give us a good estimate of this quantity. We already have answers to the second problem: in recent years, many articles have focused on developing methods to approximate certain geometric quantities on digital surfaces (such as normals or curvature), methods that we will describe in this thesis. These new approximation techniques allow us to inject measurement information into the elements of our surface. We therefore use the estimation of normals to answer the first problem, which in fact allows us to accurately approximate the tangent plane at a point on the surface and, through an integration method, to overcome topological problems related to the discrete surface. We present a theoretical convergence result of the discretized new operator, then we illustrate its properties using a numerical analysis of it. We carry out a detailed comparison of the new operator with those in the literature adapted on digital surfaces, which allows, at least for convergence, to show that only our operator has this property. We also illustrate the operator via some of these applications such as its spectral decomposition or the mean curvature flow

[pt] A primeira apresentação de um Cálculo de Seqüentes foi feita por Gerhard Gentzen na década de 1930. Neste tipo de sistema, a diferença entre as versões clássica e intuicionista radicardinalidade do sucedente. O sucedente múltiplo foi tradicionalmente considerado como o elemento que representava o aspecto clássico do sistema, enquanto os seqüentes intuicionistas podiam ter, no máximo, uma fórmula no sucedente. Nas décadas seguintes foram formulados diversos cálculos intuicionistas de sucedente múltiplo que atenuaram essa restrição forte na cardinalidade do sucedente. Na década de 1990, estudou-se a relação de conexão ou dependência entre as fórmulas visando assegurar o caráter intuicionista dos sistemas. Nós realizamos uma revisão dos sistemas de se seqüentes intuicionistas e algumas das suas aplicações. Apresentamos a versão do sistema FIL (feita para o caso proposicional por De Paiva e Pereira) para a lógica intuicionista de primeira ordem provando que o mesmo é correto, completo e satisfaz eliminação de corte. / [en] The first Sequent Calculus was presented by Gerhard Gentzen in the thirties. In this system, the difference between intuitionistic logic and classical logic is based on the cardinality of the succedent. Traditionally, the multiple succedent was considered the element that preserved the classical aspect of the system, while intuitionistic sequents have, at most, one formula in the succedent. In the following decades, several multiple succedent intuitionistic calculus were presented that diminish shed this st strong restriction in the cardinality of the su succedent. In the decade of 1990, this cardinality restriction was replaced by a dependency relation between the formula ocurrences in the antecedent and in the succedent of a sequent in order to ensure the intuitionistic character of the system. We make a revision of the intuitionistic systems and some of their applications. We present a version of the system FIL (accomplish shed for the propositional case by De Paiva and Pereira) for first-order logic proving that it is sound, complete and that it satisfies the cut-elimination theorem.

Este trabalho versa sobre técnicas de estimação de derivadas de forma não assintótica conforme abordagem algébrica de Michel Fliess, e sua aplicação na determinação quase instantânea do estado interno de um sistema dinâmico, cria-se assim estimadores de estado que não se baseiam no observador de Luenberger. Resumo No desenvolvimento do trabalho demonstramos algumas características destes estimadores e apresentamos uma contribuição teórica para viabilizar a implementação destes estimadores em sistemas de controle de tempo real. Posteriormente, um sistema mecânico de dinâmica não linear foi construído e permitiu ensaios em laboratório que atestam, através dos resultados experimentais encontrados, a funcionalidade deste tipo de estimador de estados. / This work is about derivative estimation technique based on a algebraic and non-asymptotically approach, as devised by Michel Fliess, applied on quasi-instantaneous determination of the internal state of a dynamical system, using state estimators that aren\'t based on the Luenberger observer. Abstract Over this work we present some particularities of these estimators and a theoretical contribution that will able to implement these algebraic estimators in a real time control system. After that, a non-linear mechanical system was built to verify the functionality of these state estimators.

Dans la première partie, on propose un système de type pour le lambda-calcul, dans le style du calcul des séquents, nomme « Soft Type Assignment » (STA) qui est inspiré par la logique linéaire « soft ». STA a la propriété de réduction du sujet et est correct et complète pour les calculs en temps polynomial. Par la suite on propose un déduction naturelle, STA_N. Ce système est simple mais il a le désavantage que les variables dans le sujet peuvent être explicitement renommées. Pour résoudre ce problème, on propose le système STA_M, où les contextes sont des multi-ensembles, donc les règles pour renommer les variables peuvent être interdit. L’inférence de type pour STA_M ne semble pas décidable. On propose un algorithme qui pour chaque lambda-terme rend l’ensemble de contraintes que doivent être satisfait pour que le terme soit type. Pi est correct et complet. Ensuite on étend le lambda-calcul par des constantes booléennes et on propose le système STA_B. La particularité de STA_B est que la règle du conditionnel utilise les contextes de façon additive. Chaque programme de STA_B peut être exécuté, par une machine abstraite, en espace polynomial. De plus le système est aussi complet pour PSPACE. Dans la deuxième partie, on propose une restriction de PCF, nommée SlPCF. Ce langage est équipé avec une sémantique opérationnelle qui mélange l’appelle par nom et l’appelle par valeur et peut être interprèté en mode standard dans les espaces cohérents linéaires. SlPCF est complet pour les fonctions récursives, mais il n’est pas complet et donc il n’est pas fully abstract pour les espaces cohérents linéaires / In the first part, we propose, inspired by Soft Linear Logic, a type assignment system for lambda-calculus in sequent calculus style, named Soft Type Assignment (STA). STA enjoys the subject reduction property. and is correct and complete for polynomial time computations. Then, we propose a natural deduction named STA_N. While simple, STA_N has the disadvantage of allowing the explicit renaming of variables in the subject. To overcome to this problem, we propose another natural deduction system, named STA_M, where contexts are multisets, hence rules renaming variables can be avoided. The type inference for STA_M seems in general undecidable. We propose an algorithm Pi returning, for every lambda-term, a set of constraints that need to be satisfied in order to type the term. Pi is correct and complete. We extend the lambda-calculus by basic boolean constants and we propose the system STA_B. The peculiarity of STA_B is that the conditional rule treats the contexts in an additive way. Every STA_B program can be executed, through an abstract machine, in polynomial space. Moreover, STA_B is also complete for PSPACE. In the second part we propose a restriction of PCF, named SlPCF. The language is naturally equipped with an operational semantics mixing call-by-name and call-by-value parameter passing and it can be interpreted in linear coherence space in a standard way. SlPCF is recursive complete, but it is not complete, and thus not fully abstract, with respect to linear coherence spaces

L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés / The objective of this thesis is to explore formal descriptions for the structure and functioning of biological systems, as well as formal tools for reasoning about their behavior. This work takes place in the overall prospective to study safe computational models where computations are expressed via rewriting, and where we can rely on formal verification to express and validate suitable properties. In this thesis we develop a higher-order calculus rewriting for describing molecules, reaction patterns, and biochemical network generation. The calculus is based on the chemical metaphor by describing the computations in terms of chemical solutions in which molecules representing data freely interact according to reaction rules. This way we obtained an Abstract Biochemical Calculus as an extension of the higher-order chemical model by considering structured molecules. The calculus is provided with a natural specification of concurrency and of controlling mechanisms by expressing rewrite strategies as molecules. The description of molecular complexes or chemical reactants belong to specific classes of graphs. We define the structure of port graphs and we show how the principles of the biochemical calculus instantiated for port graphs are expressive enough for modeling autonomous systems and biochemical networks. In addition, strategic rewriting techniques open the way to reason about the computations and to verify properties of the modeled systems

Made available in DSpace on 2016-04-27T14:32:37Z (GMT). No. of bitstreams: 1 Janice Valia de los Santos.pdf: 1055592 bytes, checksum: 5cc92021fe6ab3063688277e222a9174 (MD5) Previous issue date: 2009-10-29 / The present research aimed at studying the articulation of the basic formation subjects of the Engineering courses through the Differential and Integral Calculus. Thus, in this study, it was proposed a methodology which could guide the calculus activities and could be constituted as integrative experiences in the course. In order to accomplish the goals, it was also necessary to study the teachers role so as the learning process could be built. For this reason, a field research with the Differential and Integral Calculus subject, which is part of the basic formation of the Engineering course of Cruzeiro do Sul University, was developed. After accomplishing the activities, it was noticed that using integrative activities such as the ones suggested in the research by the proposed methodology is viable for the results showed the students have acquired scientific knowledge, have developed their creativity as well as basic concepts for problem solving in their specific formation / A pesquisa desenvolvida teve por objetivo estudar a articulação das disciplinas de formação básica nos cursos de engenharia por meio do Cálculo Diferencial e Integral. Desta forma, propomos, neste trabalho, uma metodologia que oriente as atividades de cálculo e que se constituam como experiências integrativas no curso. Para que atinjamos o objetivo, foi necessário estudar, também a postura do professor para que possa ser construída a aprendizagem junto ao aluno. Desse modo, desenvolvemos uma pesquisa de campo com a disciplina Cálculo Diferencial e Integral, que pertence à formação básica dos cursos de engenharia, junto aos alunos da Universidade cruzeiro do Sul. Após a realização das atividades, percebemos que é viável a utilização de atividades integrativas utilizadas na pesquisa pela metodologia proposta, visto que o aluno adquiriu conhecimento científico, desenvolveu criatividade como também conceitos básicos para a resolução de problemas em sua formação específica

Made available in DSpace on 2016-04-27T16:57:28Z (GMT). No. of bitstreams: 1 Andre Lucio Grande.pdf: 7015777 bytes, checksum: b5f1d425b769f448f927e70cdc3f11ec (MD5) Previous issue date: 2013-12-05 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The Fundamental Theorem of Calculus (FTC) occupies a prominent position in the study of Differential and Integral Calculus (DIC) as it establishes a relationship which exists between the operations of integration and differentiation as inverse to each other in addition to its use in the calculation of definite integrals, especially in solving problems which involve area, volume and arc length, amongst others. However, in the context of Mathematics Education, regarding the teaching and learning of Calculus, researches conducted in Brazil and other countries like France, England and the United States, have shown misunderstanding on the part of the students regarding the lack of connection between the concepts of Integral and Derivatives in the study of FTC. Facing this scenario, this thesis aimed at conducting a didactic and epistemological study of FTC, presenting, as its result, the elaboration and analysis of teaching intervention of which main aim was to reveal and bring up the relationship between the operations of derivation and integration and under which conditions this relationship is established as this constitutes the essence of the theorem. As a theoretical frame of reference, one has used the ideas connected to the use of intuition and rigor in the construction of mathematical knowledge according to Henri Poincaré (1995) as well as the categorizations of intuition and the interrelations between its components: the formal, algorithmic and intuitive components in mathematical activities according to Efraim Fischbein (1991). The research presented is qualitative, presenting, as methodological procedures, the development of a teaching intervention as wells as the analysis of the solutions to questions proposed by fourteen students from a technological course in a public college in the state of São Paulo with the help of Geogebra Software. In order to analyze the resolutions, besides the already mentioned theoretical frame of reference, one has also adopted the works of Tall (1991) on the role of visualization of the teaching of Calculus and the interrelationships with intuition and rigor. As results, one highlights that exploring the concepts of integral, initially by the idea of accumulation and working simultaneously with the question related to the variation of this accumulation, has shown to be a suitable strategy so that students could understand the mutual relationship between integration and derivation as operations inverse to each other, as well as it allowed them to internalize such relationship as in the genesis of FTC which came after the study of these operations. Furthermore, one can conclude that the concept of function constituted the conducting principle which guided students on the understanding of FTC. Nevertheless, difficulties in understanding the continuity of a function, one of the central points of the theorem, was also an issue which came up in the results of the teaching intervention. Analysis has shown better results on students dealing with mathematical activities when the axis of interactions among formal, algorithmic and intuitive components is dealt with the axis regarding the question of visualization in the process of teaching and learning Calculus. At the end of tasks, one has observed that students have begun to show indications of concern in order to relate intuition with rigor in the building of mathematical knowledge / O Teorema Fundamental do Cálculo (TFC) ocupa uma posição de destaque no estudo do Cálculo Diferencial e Integral (CDI), pois estabelece a relação existente entre as operações de integração e derivação como inversas entre si, além da sua utilização no cálculo de integrais definidas, em especial na resolução de problemas envolvendo área, volume e comprimento de arco, entre outras. Entretanto, no âmbito da Educação Matemática, quanto ao ensino e aprendizagem do Cálculo, pesquisas realizadas no Brasil e em outros países, tais como França, Inglaterra e Estados Unidos evidenciaram a incompreensão dos alunos no tocante à falta de ligação existente entre os conceitos de integral e derivada no estudo do TFC em um curso de Cálculo. Diante desse panorama, esta tese teve por objetivo realizar um estudo didático e epistemológico do TFC, apresentando como resultado a elaboração e análise de uma intervenção de ensino que procurou fazer emergir a relação entre as operações de integração e derivação e sob quais condições essa relação se estabelece, o que constitui a essência do teorema. Como referencial teórico foram utilizadas as ideias ligadas ao uso da intuição e do rigor na construção do conhecimento matemático, segundo Henri Poincaré (1995), bem como as categorizações da intuição e as inter-relações entre os componentes: formal, algorítmico e intuitivo nas atividades matemáticas, de acordo com Efraim Fischbein (1991). A pesquisa é qualitativa, apresentando como procedimentos metodológicos a elaboração de uma intervenção de ensino, bem como a análise das resoluções das questões efetuadas por 14 estudantes do curso de Tecnologia de uma faculdade pública do Estado de São Paulo com o auxílio do software GeoGebra. Para análise das resoluções, além do referencial teórico citado, foram adotados os trabalhos de Tall (1991) sobre o papel da visualização no ensino do Cálculo e as inter-relações com a intuição e o rigor. Como resultados, destaca-se que explorar os conceitos de integral inicialmente por meio da ideia de acumulação, simultaneamente trabalhando-se com a questão da variação dessa acumulação, mostrou-se uma estratégia pertinente para que os estudantes compreendessem a relação mútua entre integração e derivação como operações inversas uma da outra, assim como permitiu que os estudantes interiorizassem que tal relação, como ocorreu na gênese do TFC, realizou-se posteriormente ao estudo dessas operações. Além disso, pode-se concluir que o conceito de função constituiu-se na linha condutora que norteou o entendimento dos estudantes sobre o TFC. Não obstante, as dificuldades da compreensão de continuidade de uma função, um dos pontos centrais do teorema, também foi uma questão que emergiu dos resultados da intervenção de ensino. A análise mostrou melhores resultados por parte dos estudantes nas atividades matemáticas, quando o eixo das interações entre os componentes algorítmico, formal e intuitivo é trabalhado em conjunto com o eixo relacionado à questão da visualização no ensino e aprendizagem do Cálculo. No final das tarefas, observou-se que os estudantes começaram a mostrar indícios da preocupação de relacionar a intuição com o rigor na construção do conhecimento matemático

Dans cette thèse, on s'intéresse à la notion de temps fort de stationnarité et à celle, étroitement liée, de dual de stationnarité forte. Ces outils permettent d'étu- dier la convergence de processus ergodiques, en déterminant un instant aléatoire où l'équilibre est atteint. Les espaces d'état des processus considérés ici sont des graphes continus ou discrets. Dans la première partie, on considère le cas discret, et on dégage une condition nécessaire et suffisante à l'existence, pour n'importe quelle loi initiale, d'un temps fort de stationnarité fini. Pour cela, on construit explicitement un dual de station- narité forte, à valeurs dans l'ensemble des parties connexes du graphe, qui évolue à chaque étape en ajoutant ou en enlevant des points de sa frontière. Lorsque cette opération sépare l'ensemble dual en plusieurs parties, afin de ne pas le déconnecter, une de ces parties est choisie au hasard, avec une probabilité proportionnelle à son poids par la mesure invariante. On s'intéresse également au comportement général d'un processus dual, et on donne quelques exemples différents de celui construit précédemment. Dans la deuxième partie, on traite le cas continu, et le processus étudié est alors une diffusion. On caractérise notamment sa mesure invariante, et on explicite un générateur infinitésimal qui devrait être celui d'un processus dual. Néanmoins, ce cas s'avère plus compliqué que le cas discret. Le processus dual n'est donc construit que pour un mouvement brownien sur un graphe particulier, comme l'unique so- lution d'un problème de martingale. Des pistes sont présentées pour traiter des diffusions sur des graphes plus généraux, notamment en utilisant la convergence d'une suite de processus de saut tels que ceux présentés dans la première partie. / In this thesis, we are interested in the notion of strong stationary time, and in that, strongly connected, of strong stationary dual. These tools allow to study the convergence of ergodic processes, by determining a random time when the equilibrium is reached. The state space of the considered processes are discrete or continuous graphs. In the first part, we consider the discrete case, and we explicit a necessary and sufficient condition to the existence, for any initial distribution, of a finite strong stationary time. To do so, we construct explicitly a strong stationary dual, with values in the set of connected subsets of the graph, which evolves at each step by adding or removing some points at its border. Whenever this operation separates the dual set in several parts, in order not to disconnect it, one of these parts is chosen randomly, with a probability proportionnal to its weight relative to the invariant distribution. We also study the general behaviour of any dual process,2 and we give some other examples. In the second part, we deal with the continuous case, and the studied process is then a diffuion. We caracterize its invariant distribution, and we explicit an infinitesimal generator, which is expected to be that of a dual process. Nevertheless, this case turns out to be a little more involved that the discrete one. The dual process is thus constructed only for a brownian motion on a particular graph, as the unique solution of a martingale problem. Some leads are given to solve the case of diffusions on more general graphs, especially by using the convergence of a sequence of jump processes such as those presented in the first part.

The work in this thesis is inspired by the fabrication of Zn₄₅Au₃₀Cu₂₅. This is the first alloy undergoing ultra-reversible martensitic transformations and closely satisfying the cofactor conditions, particular conditions of geometric compatibility between phases, which were conjectured to influence reversibility. With the aim of better understanding reversibility, in this thesis we study the martensitic microstructures arising during thermal cycling in Zn₄₅Au₃₀Cu₂₅, which are complex and different in every phase transformation cycle. Our study is developed in the context of continuum mechanics and nonlinear elasticity, and we use tools from nonlinear analysis. The first aim of this thesis is to advance our understanding of conditions of geometric compatibility between phases. To this end, first, we further investigate cofactor conditions and introduce a physically-based metric to measure how closely these are satisfied in real materials. Secondly, we introduce further conditions of compatibility and show that these are nearly satisfied by some twins in Zn₄₅Au₃₀Cu₂₅. These might influence reversibility as they improve compatibility between high and low temperature phases. Martensitic phase transitions in Zn₄₅Au₃₀Cu₂₅ are a complex phenomenon, especially because the crystalline structure of the material changes from a cubic to a monoclinic symmetry, and hence the energy of the system has twelve wells. There exist infinitely many energy-minimising microstructures, limiting our understanding of the phenomenon as well as our ability to predict it. Therefore, the second aim of this thesis is to find criteria to select physically-relevant energy minimisers. We introduce two criteria or selection mechanisms. The first involves a moving mask approximation, which allows one to describe some experimental observations on the dynamics, while the second is based on using vanishing interface energy. The moving mask approximation reflects the idea of a moving curtain covering and uncovering microstructures during the phase transition, as appears to be the case for Zn₄₅Au₃₀Cu₂₅, and many other materials during thermally induced transformations. We show that the moving mask approximation can be framed in the context of a model for the dynamics of nonlinear elastic bodies. We prove that every macroscopic deformation gradient satisfying the moving mask approximation must be of the form 1 + a(x) ⊗ n(x), for a.e. x. With regards to vanishing interface energy, we consider a one-dimensional energy functional with three wells, which simplifies the physically relevant model for martensitic transformations, but at the same time highlights some key issues. Our energy functional admits infinitely many minimising gradient Young measures, representing energy-minimising microstructures. In order to select the physically relevant ones, we show that minimisers of a regularised energy, where the second derivatives are penalised, generate a unique minimising gradient Young measure as the perturbation vanishes. The results developed in this thesis are motivated by the study of Zn₄₅Au₃₀Cu₂₅, but their relevance is not limited to this material. The results on the cofactor conditions developed here can help for the understanding of new alloys undergoing ultra-reversible transformations, and as a guideline for the fabrication of future materials. Furthermore, the selection mechanisms studied in this work can be useful in selecting physically relevant microstructures not only in Zn₄₅Au₃₀Cu₂₅, but also in other materials undergoing martensitic transformations, and other phenomena where pattern formation is observed.

Les corrections d’ordre supérieur en dérivées applicables à la théorie de supergravité à onze dimensions constituent un puissant outil pour étudier la structure miscroscopique de la théorie M. Plus partculièrement, l’invariant supersymétrique à l’ordre huit en en dérivées est nécessaire à la cohérence quantique de la théorie, mais il n’en existe à ce jour aucune expression complète. Dans cette thèse, après une introduction formelle aux théories de supergravité, nous présentons une technique appelée principe d’action (en superespace), dont le but est de générer le superinvariant complet associé au terme de Chern-Simons d’ordre huit. Bien que ce résultat ne soit pas encore atteint, nous en déterminons certaines caratérisiques, et ouvrons la voie à une résolution systématiques des étapes de calcul à venir. Dans le chapitre suivant, nous présentons les principales fonctionnalités du programme informatique crée pour gérer les imposants calculs liés au principe d’action. Ce programme est particulièrement adapté au traitement des matrices gamma, des tenseurs et des spineurs tels qu’ils surviennent en superespace. Enfin, à l’aide de ce programme, nous abordons un autre sujet calculatoire : la condensation fermionique en supergravité IIA massive. En utilisant la formulation en superespace des supergravités IIA, nous dérivons les termes de l’action quartiques en fermions, puis en imposant une valeur moyenne dans le vide non-nulle, nous montrons qu’il est possible de construire une solution de géométrie de Sitter dans deux cas simples / High order derivative terms in eleven dimensional supergravity are a powerful tool to probe the microscopic structure of M-theory. In particular, the superinvariant at order eight in number of derivatives is required for quantum consistency, but has not been completely constructed to this day. In this thesis, after a formal introduction to supergravity, we focus on a technique called the actions principle, in superspace, with the aim of generating the full superinvariant associated to the Chern-Simons term at order eight. Although we do not construct the superinvariant, we determine some of its characteristics, and pave the way for a systematic treatment of the computations leading to the correction. Then we present the main features of the computer program we built for dealing with the computations encountered in the action principle. It is specifically designed to deal with gamma matrices, tensors and spinors as they appear in superspace. Finally, with the help of this program, we tackle another computationally intensive subject : the fermionic condensation in IIA massive superspace. We use the superspace formulations of IIA supergravitites to find the quartic fermion term of the action, and by imposing a non-vanishing vacuum expectation value for this term, we realize a de Sitter solution in two simple cases