Where do we come from and where do we go?
13 October 2020
Agda’s type checker checks correctness of our programs and proofs…
…but who checks the checker?
BUT: does not cover datatypes and pattern matching
BUT: no formally defined type system
Nice for doing optimizations
BUT: impossible to implement a type checker
MetaCoq SafeCheck, a safe-by-construction typechecker
Type : Type
My goal: develop a core language for Agda that:
The more features can be encoded, the smaller the core language can be…
… but the more complex the elaboration and the harder to understand the core code!
How to ensure new features can be added without rewriting Agda Core from scratch?