On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectivel...

Full description

Bibliographic Details
Main Author: Hyeonseung Im
Format: Article
Language:English
Published: MDPI AG 2021-02-01
Series:Mathematics
Subjects:
CPS transformation
double negation translation
simply typed lambda-calculus
propositional logic
Curry-Howard isomorphism
Online Access:https://www.mdpi.com/2227-7390/9/4/385

Internet

https://www.mdpi.com/2227-7390/9/4/385

Similar Items