A theory independent Curry-De Bruijn-Howard correspondence
Logic in Computer Science
2023-04-18 v1
Abstract
Instead of developing a customized typed lambda-calculus for each theory, we attempt to design a general parametric calculus that permits to express the proofs of any theory. This way, the problem of expressing proofs in the lambda-calculus is separated from that of choosing a theory.
Keywords
Cite
@article{arxiv.2304.08068,
title = {A theory independent Curry-De Bruijn-Howard correspondence},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2304.08068},
year = {2023}
}