Computational consistency of a formal system says that

If the sequent $\vdash e \colon (x_1 = x_2)$ is derivable (claiming a witness of the proposition of equality of two terms) then the terms $x_1$ and $x_2$ have the same value by computation.

- Alexandre Miquel,
*The experimental effectiveness of mathematical proof*(pdf)

Created on November 30, 2012 at 03:32:51. See the history of this page for a list of all contributions to it.