Ce travail présente un cadre unificateur pour les systèmes de types pour les algèbres de processus. Le cœur du système fournit une correspondance précise entre des processus essentiellement fonctionnels et des démonstrations de logique linéaire; des fragments de ce système correspondent à des connections précédemment connues entre démonstrations et processus. On montre que l'ajout d'axiomes logiques peut étendre la classe des processus typables en échange de la perte de propriétés calculatoires comme l'absence de blocage ou la terminaison, ce qui permet de voir différents systèmes connus (types i/o, linéarité, contrôle) comme des instances d'un modèle général. Cette approche suggère des méthodes unifiées pour l'extension de systèmes de types avec de nouvelles propriétés tout en restant dans un cadre bien structuré, ce qui constitue un pas vers l'étude de la sémantique dénotationnelle des processus par des méthodes de théorie de la démonstration.