GECO - Gradual verification and robust proof Engineering for COq

Equipo asociado
1

Fecha de inicio: 01-2018 

Fecha de término: 12-2022

  

Instituciones colaboradoras:

●  Equipo GALLINETTE, Inria Rennes-Bretagne Atlantique

●  Inria Chile

●  Universidad de Chile

Coordinadores:

El equipo asociado GECO está liderado por Nicolas Tabareau del equipo-proyecto GALLINETTE en Francia y en Chile por Éric Tanter, investigador del Departamento de Ciencias de la Computación (DCC) de la Universidad de Chile. Buscando aportar mejoras significativas al asistente de pruebas Coq, el equipo reúne a investigadores de Inria y de distintas instituciones en Chile (Inria Chile y Universidad de Chile).

El enfoque de este proyecto es tanto teórico como práctico, cubriendo fundamentos y métodos novedosos, diseño de lenguajes y herramientas concretas y validación a través de estudios de casos específicos. El resultado final será una serie de mejoras en el asistente de pruebas de Coq (marcos, lenguaje táctico) junto con pautas y demostraciones de su aplicabilidad en escenarios realistas.