Verimag News


  • 17 January 2019 - 14h00, Room 206 (2nd floor, badged access), by Paolo Torrini (Verimag / PACSS)
    Reifying and translating a monadic fragment of Gallina

    We present ongoing work on verified compilation of imperative functional code in Coq, relying on the CompCert C compiler and using a reflective approach. Here we focus on the reflection of a monadic fragment of Gallina, corresponding to a first-order imperative language with primitive recursion, in a deeply embedded extensible language that we call DEC2 and which can be translated to the CompCert C front-end. DEC2 has an operational interpreter based on small-step semantics, and a denotational interpreter based on its reflective (...)


  • In 4 days, Sergio Yovine (Universidad ORT Uruguay) on 21 January 2019 at 14h00 : « Formal specification and implementation of an automated pattern-based parallel-code generation framework »
  • In 5 days, Georg Struth (University of Sheffield) on 22 January 2019 at 14h00 : « Verifying Hybrid Systems with Modal Kleene Algebra »
  • In 1 week, Maiza Claire (VERIMAG) on 24 January 2019 at 14h00 : « WCET and interference analysis for multicore systems »
  • In 3 weeks, Jacques COMBAZ (CNRS, Verimag) on 7 February 2019 at 14h00 : « Assembling Components in BIP »
  • In 3 weeks (LIG Keynote) at 14h00 : Jim Roberts - Trading off memory for bandwidth in a content-centric Internet (IMAG Building Amphitheatre)