EMSOFT 2023: References to the Coq development

This page presents the artifact associated with the EMSOFT 2023 article Verified Compilation of Synchronous Dataflow with State Machines, by T. Bourke, B. Pesin, and M. Pouzet. You can also download the slides of our presentation. The following links relate the sections of the article to relevant definitions of the Coq development. The full Coq source code is available on github.

The online version of the compiler was extracted from Coq and compiled to Javascript with js_of_ocaml.

1 Introduction

The example given in the introduction can be found at examples/stepper-motor.lus.

2.1 Abstract Syntax

2.2 Synchronous Core

  • LSemantics: Lustre semantic rules
  • sem_node: Semantics of a Lustre node
  • sem_equation: Semantics of a Lustre equation
  • Svar: Semantics of a Lustre variable
  • Sconst: Semantics of a Lustre constant
  • const: Sampled constant stream
  • when coinductive operator
  • merge coinductive operator
  • wc_Ewhen: Clock-typing rule for a Lustre when
  • wc_Emerge: Clock-typing rule for a Lustre merge
  • merge_when: correspondence of when and merge
  • fby coinductive operator
  • fby1 coinductive operator
  • Sfby: Semantics of a Lustre fby

2.3 Switch Blocks

2.4 Local Scopes and Shared Variables

  • Sscope: Semantics of a local scope
  • Slast: Semantics of a last expression
  • union operator on histories

2.5 Reset Blocks

  • mask coinductive operator
  • mask_hist: mask lifted on histories.
  • Sreset: Semantics of a reset block

2.6 State Machines

  • select coinductive operator
  • SautoWeak: Semantics of a state machine with weak transitions
  • SautoStrong: Semantics of a state machine with strong transitions
  • sem_transitions: Semantics of state machines transitions and initializations
  • choose_first (first-of) coinductive operator

3.1 Dependency Analysis and Instrumented Semantic Model

3.2 Shared Variables

3.3 State Machines

3.4 Switch Blocks

3.5 Local Scopes

3.6 Reset Blocks