The concept of syntactical duality is central in logic. In particular, the duality defined by classical negation, or more syntactically by left and right in sequents, has been widely used to relate logic and computations. We study the proof/test duality proposed by Girard in his 1999 paper on the meaning of logical rules. In detail, starting from the notion of “test” proposed by Girard, we develop a notion of test for intuitionistic logic and we give a complete deductive system whose computational interpretation is the target language of the call-by-value and call-by-name continuation passing style translations.
Proofs, tests and continuation passing style
MASINI, Andrea
2009-01-01
Abstract
The concept of syntactical duality is central in logic. In particular, the duality defined by classical negation, or more syntactically by left and right in sequents, has been widely used to relate logic and computations. We study the proof/test duality proposed by Girard in his 1999 paper on the meaning of logical rules. In detail, starting from the notion of “test” proposed by Girard, we develop a notion of test for intuitionistic logic and we give a complete deductive system whose computational interpretation is the target language of the call-by-value and call-by-name continuation passing style translations.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
