Implicit and noncomputational arguments using monads
Pierre Letouzey, Bas Spitters · 2005
Abstract. We provide a monadic view on implicit and noncomputa-tional arguments. This allows us to treat Berger’s non-computational quantifiers in the Coq-system. We use Tait’s normalization proof and the concatenation of vectors as case studies for the extraction of pro-grams. With little effort one can eliminate noncomputational arguments from extracted programs. One thus obtains extracted code that is not only closer to the intended one, but also decreases both the running time and the memory usage dramatically. We also study the connection be-tween Harrop formulas, lax modal logic and the Coq type theory.