Auteur : Jocelyn Sérot  (Dream - UBP) 

Titre : Théorie des types pour les concepteurs de circuits. Le cas du langage CAPH.
  
Abstract : 

CAPH (caph.univ-bpclermont.fr) est un DSL dédié à la synthèse haut niveau d'applications sur circuits FPGA. Son but est de permettre à des programmeurs que l'usage des langages de description de matériel (VHDL, Verilog) d'exploiter ce type de plateforme. S'appuyant sur un modèle de programmation de type flot de données, CAPH emprunte largement aux langages fonctionnels. Le comportement des acteurs constituant les applications, notamment, y est défini comme une collection de règles opérant selon un mécanisme de pattern matching très similaire à celui que l'on trouve les langages de la famille ML ou Haskell. Par ailleurs, le formalisme de description des graphes est lui-même un petit langage purement fonctionnel, polymorphique et d'ordre supérieur. 
Dans cet exposé, on présentera rapidement les motivations, principes et modus operandi du langage puis on se focalisera sur les aspects liés au typage. Ces aspects prennent en effet un importance toute particulière lorsque le code généré cible explicitement du matériel. Deux points en particulier seront présentés. D'une part les techniques utiliséss pour compiler la pleine fonctionnalité et le polymophisme vers des langages moins riches comme SystemC ou VHDL. D'autre part, la définition et la mise en oeuvre d'une extension du système classique introduit par Hindley et Millner supportant la notion d'entiers paramétrés par leur taille (en bits), extension qui peut être vue comme une forme minimale d'un système de types dépendants.