GECO - Gradual verification and robust proof Engineering for COq

The associate GECO team is led by Nicolas Tabareau from the GALLINETTE project-team in France and in Chile by Éric Tanter, a researcher at the Department of Computer Science (DCC) of the University of Chile. Seeking to provide significant improvements to the Coq test assistant, the team brings together researchers from Inria and from different institutions in Chile (Inria Chile and University of Chile).

The focus of this project is both theoretical and practical, covering fundamentals and novel methods, language design and concrete tools, and validation through specific case studies. The end result will be a series of improvements to the Coq test wizard (frameworks, tactical language) along with guidelines and demonstrations of its applicability in realistic scenarios.