@Inproceedings{EPTCS275.2, author = {Pope, Jeremy}, year = {2018}, title = {Formalizing Constructive Quantifier Elimination in Agda}, editor = {Atkey, Robert and Lindley, Sam}, booktitle = {{\rm Proceedings of the 7th Workshop on} Mathematically Structured Functional Programming, {\rm Oxford, UK, 8th July 2018}}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {275}, publisher = {Open Publishing Association}, pages = {2-17}, doi = {10.4204/EPTCS.275.2}, }