Journal of Symbolic Logic · 2003 · 11 citations · 2 references
ComputingComputer ScienceMathematicsFormal MethodsDeductive ReasoningPredicate LogicTheorem ProvingFormal Proof SystemsNormalization
Abstract This paper points out an error of Parigot's proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.
2
Call-by-name, call-by-value and the λ-calculus
Gordon Plotkin · Theoretical Computer Science · 1975 · 1.2K citations
Ken-etsu Fujita · RAIRO - Theoretical Informatics and Applications · 2000 · 10 citations