nLab pi-r-squared team

This is a research group formed within PPS, working on rewriting and Coq.

The team $\pi r^2$ covers three research topics:

• Fundamental research concerning the correspondence between proofs and programs

• Theoretical research on the formalism that underlies the Coq proof assistant

• An implementation research field with the development of Coq, especially in the view of Coq as dependently-typed programming language

References

• homepage