El cálculo de construcciones sirvió de base a las primeras versiones del demostrador de teoremas Coq; las versiones posteriores se construyeron sobre el cálculo de Construcciones Inductivas que es una extensión de CoC con soporte para tipos de datos inductivos.