We have a pleasure to invite you to our FIL Talks that will be hold on July, 6 at 15h00-16h00.

When: 6th of July, 15h00-16h00

Where: Campus de Gerland – ENS Lyon – Laboratoire LIP
3ème étage – Salle de conseil
46 All. d’Italie, 69007 Lyon

Attending online: BBB link

———————————————–
Talk by: Romain Michon

Title: Quick and Easy Programming of FPGA Platforms for Real-Time Audio Signal Processing Applications

Keywords: Audio Digital Signal Processing ; FPGA ; Domain Specific Languages

Abstract:
FPGAs offer a wide range of new exciting possibilities for real-time audio signal processing applications such as ultra-low audio latency, management of large numbers of parallel audio channels, audio computations at a high sampling rate, spatial audio, etc. However, programming them in this context remains a relatively hard task which is out of reach to most DSP engineers, hobbyists, etc. As part of the FAST project (Fast Audio Signal-processing Technologies on FPGA) we (the INRIA Emeraude Team) are developing a toolchain to program FPGA platforms for real-time audio applications with the Faust programming language. In this presentation, an overview of this new system and of what it has to offer will be given.

Speaker bio:
Romain Michon is faculty researcher at INRIA (Emeraude Team), associate researcher at GRAME — Centre National de Création Musicale in Lyon (France), and lecturer at the Center for Computer Research in Music and Acoustics (CCRMA) at Stanford University (USA). He has been involved in the development of the Faust programming language since 2008 and he’s now part of the core Faust development team at GRAME. Romain’s research interests involve embedded systems for real-time audio processing, Human Computer Interaction (HCI), New Interfaces for Musical Expression (NIME), and physical modeling of musical instruments.

———————————————–

Talk by: Yannick Zakowski

Title: Vellvm: a Compositional, Modular, Executable Semantics for LLVM IR

Keywords: coq; semantics; compiler verification

Abstract:
Compiler verification is the art of programming and proving in a proof assistant a compiler guaranteed to faithfully transport the semantics of the source program down to its target language. Through this talk, we will introduce the general concepts underlying this field, before focusing more specifically on Vellvm, an ongoing formalization in the Coq proof assistant of LLVM IR, the intermediate representation used by the LLVM compiling infrastructure.

Speaker bio:
Yannick Zakowski is CR Inria recruited in 2020 after a postdoc at UPenn in the US and a PhD at ENS Rennes in France. Particularly interested in compiler verification and semantics.