JFLA 2026: Références au développement Rocq

Cette page présente le développement associé à la soumission "Une sémantique de Kahn mécanisée pour les machines à états" pour les JFLA 2026. Les liens suivants mettent en relation les sections de l'article avec les définitions Rocq correspondantes. Le développement complet est disponible.

Les noms sont susceptibles de différer entre l'article et le code source. Les liens réfèrent aux noms de l'article et les noms Rocq sont donnés entre parenthèses.

2.1 Syntaxe abstraite

• expressions
• blocs
• nœuds

3 La bibliothèque CPO

Importé depuis le site de C. Paulin-Mohring.

3.1 Ordres complets partiels

• ord: type ordonné
• monotonic: monotonicité
• cpo: CPO
• continuous : continuité
• FIXP : opérateur de point fixe défini comme une fonction continue

3.2 Flots et réseaux de Kahn

• DStr : le type des flots

• DS_bot: le flot vide

• DS: le CPO des flots

• DSle, l'ordre préfixe sur les flots

• Les opérateurs REM, fby (APP), MAP, merge, wheni.

• value

• evalue(errv)

• SEnv : le type des environnements de flots

• union_left (union_env)

• FEnv : le type des fonctions d'environnements

• denot_exp_eq (kdenot_exp_eq) : dénotation d'une expression

• denot_block_eq (kdenot_block_eq) : dénotation d'un bloc

• denot_node_eq (kdenot_node_eq) : dénotation d'un nœud

• denot_global_eq (kdenot_global_eq) : dénotation d'un programme

4 Extension aux machines à états

4.1 Transitions sans réinitialisation

• mergei
• mergei_cons
• switch
• switch_eq
• auto_continue_strong
• auto_continue_strong_eq
• auto_continue_weak_eq

4.2 Transitions avec réinitialisation

• rem_unless
• rem_until
• mergei_unless
• mergei_until
• auto_reset_weak_eq
• auto_reset_strong_eq

4.3 Transitions mixtes

• auto_weak_eq
• auto_strong_eq