https://www.sciencedirect.com/science/article/pii/S016800721200084X
Towards a canonical classical natural deduction system
JoséEspírito Santo
This paper studies a new classical natural deduction system, presented as a typed calculus. It is designed to be isomorphic to Curien and Herbelinʼs-calculus, both at the level of proofs and reduction, and the isomorphism is based on the correct correspondence between cut (resp. left-introduction) in sequent calculus, and substitution (resp. elimination) in natural deduction. It is a combination of Parigotʼs λμ-calculus with the idea of “coercion calculus” due to Cervesato and Pfenning, accommodating let-expressions in a surprising way: they expand Parigotʼs syntactic class of named terms.
Towards a canonical classical natural deduction system
JoséEspírito Santo
This paper studies a new classical natural deduction system, presented as a typed calculus. It is designed to be isomorphic to Curien and Herbelinʼs-calculus, both at the level of proofs and reduction, and the isomorphism is based on the correct correspondence between cut (resp. left-introduction) in sequent calculus, and substitution (resp. elimination) in natural deduction. It is a combination of Parigotʼs λμ-calculus with the idea of “coercion calculus” due to Cervesato and Pfenning, accommodating let-expressions in a surprising way: they expand Parigotʼs syntactic class of named terms.