IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2017 > Reasoning Techniques for the Module System Formalisation in Coq
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Danil Annenkov

martes 26 de septiembre de 2017

10:45am Meeting room 302 (Mountain View), level 3

Danil Annenkov, PhD Student, DIKU University of Copenhagen, Denmark

Reasoning Techniques for the Module System Formalisation in Coq


In this talk we present a number of techniques that allow for formal reasoning with nested and mutually inductive structures built up from finite maps and sets (also called semantic objects), and at the same time allow for working with binding structures over sets of variables. The techniques, which build on the theory of nominal sets combined with the ability to work with multiple isomorphic representations of finite maps, make it possible to give a formal treatment, in Coq, of a higher-order module system, including the ability to eliminate entirely, at compile time, abstraction barriers introduced by the module system. The development is based on earlier work on static interpretation of modules and provides the foundation for a higher-order module language for Futhark, an optimising compiler targeting data-parallel architectures, such as GPGPUs.