Email Gateway (Aug 22 2022 at 15:53): Email Gateway (Aug 22 2022 at 15:53):From: Tobias Nipkow <nipkow@in.tum.de>
The λμ-calculus
Cristina Matache, Victor B. F. Gomes, and Dominic P. Mulligan
The propositions-as-types correspondence is ordinarily presented as linking the
metatheory of typed λ-calculi and the proof theory of intuitionistic logic.
Griffin observed that this correspondence could be extended to classical logic
through the use of control operators. This observation set off a flurry of
further research, leading to the development of Parigots λμ-calculus. In this
work, we formalise λμ- calculus in Isabelle/HOL and prove several
metatheoretical properties such as type preservation and progress.
https://www.isa-afp.org/entries/LambdaMu.html
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC