TY  - RPRT
TI  - Formalizing Constructive Quantifier Elimination in Agda
AU  - Jeremy Pope
PY  - 2018
DO  - 10.4204/eptcs.275.2
UR  - https://arxiv.org/abs/1807.04083
ID  - 1807.04083
ER  -