Internship proposals

Local extensions of type theory

When dealing with certain domains or theories, proof assistants sometimes lack the necessary support to make proofs easy. Sometimes, such theories rely on specific models to make sense, and are thus not compatible with other approaches. People thus develop plugins or even dedicated proof assistants to better suit their needs.

Ideally, I think general purpose proof assistants should support the design of embedded domain-specific proof assistants in a way that doesn’t preclude interaction with the rest of the ecosystem. I have recently started working in this direction with Yann Leray (see “Encode the Cake and Eat it Too: Controlling computation in type theory, locally” below) by designing a way to abstract not only over assumptions but also over computation (definitional equality) in type theory.

I propose to go further towards DSLs by also supporting the creation of universes and the ability to create models for a specific universe using a parametricity translation.