Achievements and Planned Activities

Ongoing research

  • Hybrid and gradual verification in proof assistants

    Study the foundations of hybrid and gradual verifications in proof assistants to allow smoothly combining static and dynamic verification in an expressive setting.

  • Gradual Indexed Inductive Types

    Extending the Gradual Calculus of Inductive Constructions (GCIC) with support for indexed inductive types and implementing a prototype in Coq.

  • Internal reasoning about precision and graduality in proof assistants

    Study and further develop the ideas of internalizing precision and graduality, extending them to other gradual variants of the CIC, in order to demonstrate its benefits.

Code

  • GCIC prototype implementation

    A prototype implementation of GCIC written in OCaml.

  • GRIP prototype implementation in Coq

    A prototype implementation of the cast-calculus for GCIC (GRIP) written in Coq itself, using different extension mechanisms.

Publications

No publications yet

Talks

Prior related joint work