[Parigot 1992] introduced the -calculus as a system for classical logic.
In terms of programming, the -calculus is a -calculus equipped with continuation variables, to which one can throw values, or capture them using binding.
The -calculus has two sorts of typing judgments:
In either case, is the usual context of variables , while is a context of continuation variables .
The idea is that the first sequent is the usual intuitionistic one, stating that is a term that computes a value of type using continuation variables in . Meanwhile, the second sequent corresponds to a command, which does some "internal" computation.
The type system is given by the following rules, which are slightly adapted from the original system by [Ariola and Herbelin 2003]:
The first three rules are the usual rules of the simply-typed -calculus. They have an extra context added to them parametrically.
The last two rules are the classical rules. The first one is sometimes called the passivate rule, and the second one the activate rule.
Read logically, assumptions in can be understood as proofs of . Then the rules capture the following intuitions:
Seen more operationally:
It is an instructive exercise to show that Peirce's law is typable as the term
Very roughly, the operational behaviour of this can be described as follows: in trying to produce an :
Notice that the fact that persists even after one throws something at it in the passivate rule is crucial for typing this example.
There are two dynamics for the calculus.
In either case, the substitution operator
replaces every subterm of the form with the subterm . Similarly for .
The presentation here has been adapted from [Ariola and Herbelin 2003].
Let be a value, i.e. a variable or a -abstraction.
There is a Wikipedia page on the -calculus.
The -calculus was introduced in the paper
Parigot, Michel. 1992. ‘λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction’. In Logic Programming and Automated Reasoning, edited by Andrei Voronkov, 624:190–201. Lecture Notes in Computer Science. Berlin/Heidelberg: Springer-Verlag. https://doi.org/10.1007/BFb0013061.
@inproceedings{parigot_1992,
address = {Berlin/Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {$\lambda\mu$-{Calculus}: {An} algorithmic interpretation of classical natural deduction},
volume = {624},
doi = {10.1007/BFb0013061},
booktitle = {Logic {Programming} and {Automated} {Reasoning}},
publisher = {Springer-Verlag},
author = {Parigot, Michel},
editor = {Voronkov, Andrei},
year = {1992},
pages = {190--201}
}
Parigot, Michel. 1997. ‘Proofs of Strong Normalisation for Second Order Classical Natural Deduction’. Journal of Symbolic Logic 62 (4): 1461–79. https://doi.org/10.2307/2275652.
@article{parigot_1997,
title = {Proofs of strong normalisation for second order classical natural deduction},
volume = {62},
doi = {10.2307/2275652},
number = {4},
journal = {Journal of Symbolic Logic},
author = {Parigot, Michel},
year = {1997},
pages = {1461--1479}
}
Ong, C.-H. L., and C. A. Stewart. 1997. ‘A Curry-Howard Foundation for Functional Computation with Control’. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’97, 215–27. ACM Press. https://doi.org/10.1145/263699.263722.
@inproceedings{ong__1997,
title = {A {Curry}-{Howard} foundation for functional computation with control},
doi = {10.1145/263699.263722},
booktitle = {Proceedings of the 24th {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages} - {POPL} '97},
publisher = {ACM Press},
author = {Ong, C.-H. L. and Stewart, C. A.},
year = {1997},
pages = {215--227}
}
Ariola, Zena M., and Hugo Herbelin. 2003. ‘Minimal Classical Logic and Control Operators’. In Automata, Languages and Programming, edited by Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, 2719:871–85. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-45061-0_68. [slides]
@inproceedings{ariola_2003,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Minimal {Classical} {Logic} and {Control} {Operators}},
volume = {2719},
doi = {10.1007/3-540-45061-0_68},
booktitle = {Automata, {Languages} and {Programming}},
publisher = {Springer Berlin Heidelberg},
author = {Ariola, Zena M. and Herbelin, Hugo},
editor = {Baeten, Jos C. M. and Lenstra, Jan Karel and Parrow, Joachim and Woeginger, Gerhard J.},
year = {2003},
pages = {871--885}
}