index.html

---
layout: default
publication_limit: 5
---

<main class="flex flex-col space-y-6">
  <section class="pt-4">
    <p>
      <em>GRAPA</em> (short for GRAdual Proof Assistants) is an associate team
      between the Inria Project-Team
      <a href="https://gallinette.gitlabpages.inria.fr/website/">Gallinette</a>,
      led by <a href="https://tabareau.fr/">Nicolas Tabareau</a>, and the
      <a href="https://www.pleiad.cl">Pleiad</a> laboratory of the University of
      Chile, led by <a href="https://pleiad.cl/etanter/">Éric Tanter</a>.
    </p>
    <p>GRAPA is the continuation of a joint line of work between our teams 
      on making proof assistants more 
      accessible by combining static and dynamic checking, combining our expertise on 
      proof assistants on the one hand, and gradual typing on the other hand.
  </section>

  <section>
    <h2 class="mb-4">Project</h2>

    <p>
      <em>GRAPA</em> aims at extending the reach of gradual typing to
      full-fledged type theories in order to support smooth certified
      programming in a new generation of proof assistants.
    </p>
    <p>
      More specifically, our current objectives are organized around two axes:
    </p>
    <ul class="pl-8 list-disc text-justify">
      <li class="py-1">
        Foundations of Gradual Type Theory: we develop the foundations of gradual type theory
        by extending prior work on gradual typing to deal with dependent types as found in the type theories underlying
        modern proof assistants such as 
        <a href="https://coq.inria.fr">Coq</a>, 
        <a href="https://agda-lang.org">Agda</a> and 
        <a href="https://leanprover.github.io/">Lean</a>. In particular we focus on the Calculus of Inductive Constructions (CIC) and
        its extensions.
      </li>
      <li class="py-1">
        Internal Reasoning about Precision and Graduality: we will further
        develop the ideas of internalizing precision and graduality, building
        upon recent work on observational equality, and extending to other
        gradual variants of CIC (e.g. with global graduality) in order to
        demonstrate its benefits.
      </li>
      <li class="py-1">
        Implementations of Gradual Type Theory: we will explore alternatives
        to implement gradual proof assistants, in particular using extension mechanisms
        such as rewrite rules and macros.
      </li>
      <li class="py-1">
        Gradual Verification in Proof Assistants: we will study how to make a program logic 
        such as that of <a href="https://iris-project.org/">Iris</a> more flexible through hybrid and gradual checking techniques.
      </li>
    </ul>
  </section>

  <section class="">
    <h2 class="mb-4">News</h2>
    {% include news-list.html %}
  </section>
</main>