# Adding Negation to Lambda Mu

@article{Bakel2021AddingNT, title={Adding Negation to Lambda Mu}, author={Steffen van Bakel}, journal={ArXiv}, year={2021}, volume={abs/2109.10447} }

We present L, an extension of Parigot’s λμ-calculus by adding negation as a type constructor, together with syntactic constructs that represent negation introduction and elimination. We will define a notion of reduction that extends λμ’s reduction system with two new reduction rules, and show that the system satisfies subject reduction. Using Aczel’s generalisation of Tait and Martin-Löf’s notion of parallel reduction, we show that this extended reduction is confluent. Although the notion of…

#### Figures from this paper

#### References

SHOWING 1-10 OF 48 REFERENCES

Exception Handling and Classical Logic

- Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019
- 2019

We present λtry, an extension of the λ-calculus with named exception handling, via try, throw and catch, and present a basic notion of type assignment expressing recoverable exception handling and…

Intersection Types for the λμ-Calculus

- 2014

We introduce an intersection type system for the λμ-calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus’s denotational model of…

A Curry-Howard foundation for functional computation with control

- Computer SciencePOPL '97
- 1997

The goal is that ¿µv and µPCFv respectively should be to functional computation with first-class access to the flow of control what ¿-calculus and PCF respectively are to pure functional programming.

Curry-Howard Term Calculi for Gentzen-Style Classical Logics

- Computer Science
- 2008

This thesis believes this is the first time a general notion of cut-elimination for classical sequent calculus has been encoded into a calculus based on a Gentzen-style presentation of classical natural deduction.

Parallel Reduction in Type Free lambda/mu-Calculus

- Mathematics, Computer ScienceElectron. Notes Theor. Comput. Sci.
- 2001

It is shown that the new formulation of parallel reduction has the diamond property, which yields a correct proof of the confluence for type free λμ-calculus.

Classical Logic, Continuation Semantics and Abstract Machines

- Computer ScienceJ. Funct. Program.
- 1998

This paper derives the transition rules for an abstract machine from a continuation semantics which appears as a generalization of the ¬¬-translation known from logic.

A proof-theoretic foundation of abortive continuations

- Mathematics, Computer ScienceHigh. Order Symb. Comput.
- 2007

Abstract
We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce’s law without enforcing Ex Falso Quodlibet. We show that a “natural”…

Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction

- Computer ScienceLPAR
- 1992

This paper presents a way of extending the paradigm "proofs as programs" to classical proofs, which can be seen as a simple extension of intuitionistic natural deduction, whose algorithmic interpretation is very well known.

A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework

- Computer Science
- 1992

A detailed, informal proof of the Church-Rosser property for the untyped lambda-calculus is given and its representation in LF is shown.

Minimal Classical Logic and Control Operators

- Computer Science, MathematicsICALP
- 2003

An analysis of various classical axioms is given and a notion of minimal classical logic that enforces Peirce's law without enforcing Ex Falso Quodlibet is characterized, showing that a "natural" implementation of this logic is Parigot's classical natural deduction.