# Class of functions computable by Coq

Since it does not allow nonterminating computation, Coq is necessarily not Turing-complete. What is the class of functions that Coq can compute? (is there an interesting characterization thereof?)

• You can use the constructive lift monad, $A_\bot \triangleq \nu \alpha.\; A + \alpha$, to write general recursive functions. Then your typechecker will have type $\mathsf{context} \to \mathsf{term} \to \mathsf{type} \to \mathsf{bool}_\bot$. This is basically the Bove/Capretta approach. (See also Benton, Kennedy and Varming's "Some Domain Theory and Denotational Semantics in Coq", dl.acm.org/citation.cfm?id=1616077.1616090.) Jan 19 '12 at 5:39