Les neurones biologiques communiquent par le biais d’impulsions électriques, appelées spikes, et les fonctions cérébrales émergent notamment de la coordination entre les réceptions et émissions de ces spikes. Par ailleurs, il est largement admis que la fonction de chaque neurone dépend de sa morphologie. Les dendrites conditionnent l’intégration spatio-temporelle des spikes reçus et influent sur les temps d’occurrence des spikes émis. Elles sont donc fondamentales pour l’étude in silico des mécanismes de coordination, et en particulier pour l’étude des assemblées de neurones. Les modèles de neurones existants prenant en compte les dendrites, sont généralement des modèles mathématiques détaillés, souvent à base d’équations différentielles, dont la simulation nécessite des ressources de calculs importantes. De plus, leur complexité intrinsèque rend difficile l’analyse et les preuves sur ces modèles. Dans cette thèse, nous proposons un modèle de neurone intégrant des dendrites d’une manière abstraite. Dans l’objectif d’ouvrir la porte aux méthodes formelles, nous établissons une définition rigoureuse du cadre de modélisation et mettons en évidence des propriétés algébriques remarquables de l’intégration dendritique. Nous avons notamment démontré qu’il est possible de réduire la structure d’un neurone en préservant sa fonction d’entrée/sortie. Nous avons ainsi révélé des classes d’équivalence dont nous savons déterminer un représentant canonique. En s’appuyant sur la théorie des catégories et par des morphismes de neurones judicieusement définis, nous avons ensuite analysé plus finement ces classes d’équivalence. Un résultat surprenant découle de ces propriétés : un simple ajout de délais dans les modèles informatiques de neurones permet de prendre en compte une intégration dendritique abstraite, sans représenter explicitement la structure arborescente des dendrites. À la racine de l’arborescence dendritique, la modélisation du soma contient inévitablement une équation différentielle lorsque l’on souhaite préserver l’essence du fonctionnement biologique. Ceci impose de combiner une vision analytique avec la vision algébrique. Néanmoins, grâce à une étape préalable de discrétisation temporelle, nous avons également implémenté un neurone complet en Lustre qui est un langage formel autorisant des preuves par model checking. Globalement, nous apportons dans cette thèse un premier pas encourageant vers une formalisation complète des neurones, avec des propriétés remarquables sur l’intégration dendritique. / Biological neurons communicate by means of electrical impulses, called spikes. Brain functions emerge notably from reception and emission coordination between those spikes. Furthermore, it is widely accepted that the function of each neuron depends on its morphology. In particular, dendrites perform the spatio-temporal integration of received spikes and affect the occurrence of emitted spikes. Dendrites are therefore fundamental for in silico studies of coordination mechanisms, and especially for the study of so-called neuron assemblies. Most of existing neuron models taking into account dendrites are detailed mathematical models, usually based on differential equations, whose simulations require significant computing resources. Moreover, their intrinsic complexity makes difficult the analysis and proofs on such models. In this thesis, we propose an abstract neuron model integrating dendrites. In order to pave the way to formal methods, we establish a rigorous definition of the modeling framework and highlight remarkable algebraic properties of dendritic integration. In particular, we have demonstrated that it is possible to reduce a neuron structure while preserving its input/output function. We have thus revealed equivalence classes with a canonical representative. Based on category theory and thanks to properly defined neuron morphisms, we then analyzed these equivalence classes in more details. A surprising result derives from these properties: simply adding delays in neuron computational models is sufficient to represent an abstract dendritic integration, without explicit tree structure representation of dendrites. At the root of the dendritic tree, soma modeling inevitably contains a differential equation in order to preserve the biological functioning essence. This requires combining an analytical vision with the algebraic vision. Nevertheless, thanks to a preliminary step of temporal discretization, we have also implemented a complete neuron in Lustre which is a formal language allowing proofs by model checking. All in all, we bring in this thesis an encouraging first step towards a complete neuron formalization, with remarkable properties on dendritic integration.