Specifying programs with propositions and with congruences
Logic in Computer Science
2023-04-27 v1
Abstract
We give a presentation of Krivine and Parigot's Second-order functional arithmetic in Deduction modulo. Expressing this theory in Deduction modulo sheds light on an original aspect of this theory: the fact that programs are specified, not with propositions, but with congruences.
Keywords
Cite
@article{arxiv.2304.13321,
title = {Specifying programs with propositions and with congruences},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2304.13321},
year = {2023}
}