Lafont translation

The Lafont translation is a translation from classical propositional logic to the (\lnot, \land) fragment of propositional intuitionistic logic.

It can also be understood as a CPS translation of a call-by-name \lambda-calculus with control to a \lambda-calculus for the (\lnot, \land) fragment of intuitionistic logic.

This was extended to a a CPS translation version of PCF by Lafont, Streicher, Reus 1993.

References

• The Lafont translation appears to have been introduced in an unpublished manuscript, which is difficult to locate.

• Most of the information here is drawn from

Chicago

Streicher, Th., and B. Reus. 1998. ‘Classical Logic, Continuation Semantics and Abstract Machines’. Journal of Functional Programming 8 (6): 543–72. https://doi.org/10.1017/S0956796898003141.

BibTeX

@article{streicher_classical_1998,
	title = {Classical logic, continuation semantics and abstract machines},
	volume = {8},
	doi = {10.1017/S0956796898003141},
	number = {6},
	journal = {Journal of Functional Programming},
	author = {Streicher, Th. and Reus, B.},
	year = {1998},
	pages = {543--572}
}