Seminar Programme (TBD)

As usual, the technical programme is created and updated dynamically as we proceed. The current version is available via the following link. Here, we currently only mention the basic schedule.

Monday 18/Nov/24

Tuesday 19/Nov/24

Wednesday 20/Nov/24

Thursday 21/Nov/24

Friday 22/Nov/24

• Jean Baptiste Jeannin, Department of Aerospace Engineering, University of Michigan at Ann Arbor, USA
  
  Synchronous Programming with Refinement Types
  
  This talk will present MARVeLus, a cyber-physical systems language which combines verification, simulation, and implementation. The language is based on Zélus, a modern version of Lustre, where we add refinement types and associated typing rules. Our refinement types can express temporal-logic-based safety properties and prove them using a rich type system in the style of deductive verification. The language comes with an implementation, and a platform enabling execution on physical robots. Although our current implementation is limited to verifying properties about discrete constructs of Zélus, the talk will also present early efforts extending the proof systems to continuous constructs of Zélus, inspired by the theory of differential dynamic logic.
   
• Romain Michon, INRIA, INSA Lyon, Centre Nationale de Création Musicale (GRAME), France
  
  Evolution of Real-Time Audio Signal Processing Through the Lens of Timing and Synchronicity
  
  From the early ages of music to advanced virtual acoustics rendering systems used in nowadays' concert halls, timing and synchronicity always played a central role in the context of human-made sound production. This evolution culminated during the second half on the twentieth century with real-time digital audio signal processing systems which can now be found everywhere in our day-to-day life: smartphones, televisions, laptops, cars, virtual reality systems, etc. In this talk, we start by examining how complex rhythmic structures in music helped to solidify our understanding of clocking systems. We demonstrate that latency always played a central role in sound production, from large organs in highly reverberant churches to systems for room acoustics active control requiring sub-millisecond latency. Finally, we give an overview of the state of the art of modern technologies for real-time audio signal processing, before presenting ongoing research carried out in this very active field. Throughout this presentation, we also emphasize how the fields of music and audio in general have always been following the technological progresses that shaped their time.  
  
   
• Koen Claessen, Chalmers University of Technology, Gothenburg, Sweden
  
  Combining Functional Reactive Programming and Lustre

  
  We are interested in methods for programming small IoT devices that run on batteries. We regard these as reactive real-time systems that (1) can react to external events that happen occasionally (such as sensors that trigger), (2) must have precise timing behavior, and (3) are otherwise mostly asleep for power reasons. We have previously developed a language called Scoria (based on the Sparse Synchronous Model) that tries to fill this niche. However, Scoria is an imperative language with processes that can be started dynamically, which means no guarantees about bounded memory and no easy route to formal verification.
  
  In this talk, we explore how we can use a more declarative approach to this problem, with run-time guarantees about timing and bounded memory behavior, and enabling formal verification easily. An obvious choice is to use Lustre; however the semantics (a clock that always ticks) and typical implementations of Lustre do not fit well with only reacting to external events and otherwise being asleep. Functional Reactive Programming (FRP) provides key semantic concepts for declarative reasoning about reactive systems, but its existing implementations are way too expressive to have any runtime guarantees close to the guarantees of Lustre. We have developed a restricted variant of FRP specifically targeted to be used in a Lustre-like language that allows for a declarative style of programming reactive (and mostly at-rest) real-time systems while at the same time guaranteeing bounded memory use, and enabling easy formal verification.
  
  These ideas have all been implemented in a rough prototype language embedded in Haskell called Frustre.