Specification, formalization and verification of the XC function from ex lambda calculus[1]. The main work is done in xc.v file.
[1] https://www.irif.fr/~kesner/papers/safe-full-composition.pdf
Specification, formalization and verification of the XC function from ex lambda calculus[1]. The main work is done in xc.v file.
[1] https://www.irif.fr/~kesner/papers/safe-full-composition.pdf