Back to Search Start Over

Specifying programs with propositions and with congruences

Authors :
Dowek, Gilles
Inria Saclay - Ile de France
Institut National de Recherche en Informatique et en Automatique (Inria)
Publication Year :
2023
Publisher :
arXiv, 2023.

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.

Subjects

Subjects :
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Logic in Computer Science (cs.LO)

Details

Database :
OpenAIRE
Accession number :
edsair.doi.dedup.....fcb346e082de75656c9a51efe5b7a943
Full Text :
https://doi.org/10.48550/arxiv.2304.13321
Full Text Access
View/download PDF

Tools

Authors Abstract Subjects Details