Adding Negation to Lambda Mu

DOI10.46298/LMCS-19(2:12)2023MaRDI QIDQ6135761zbMATH OpenOpenAlexFDO

Authors

Publication date 26 August 2023

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2109.10447

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Abstract: We present $calL$, an extension of Parigot's $lambdamu$-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 $lambdamu$'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"of's notion of parallel reduction, we show that this extended reduction is confluent. Although the notion of type assignment has its limitations with respect to representation of proofs in natural deduction with implication and negation, we will show that all propositions that can be shown in there have a witness in $calL$. Using Girard's approach of reducibility candidates, we show that all typeable terms are strongly normalisable, and conclude the paper by showing that type assignment for $calL$ enjoys the principal typing property.

Recommendations

• Reduction system for extensional lambda-mu calculus
• scientific article; zbMATH DE number 1670497
• Normalization in the simply typed -calculus
• scientific article; zbMATH DE number 1722654
• The differential \(\lambda \mu\)-calculus

Cites work

• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• A Machine-Oriented Logic Based on the Resolution Principle
• A proof-theoretic foundation of abortive continuations
• Characterisation of normalisation properties for using strict negated intersection types
• Classical logic, continuation semantics and abstract machines
• Functionality in Combinatory Logic
• Gentzen's Proof of Normalization for Natural Deduction
• scientific article; zbMATH DE number 3485716 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 2038761 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3348059 (Why is no real title available?)
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Intensional interpretations of functionals of finite type I
• Intersection types for the -calculus
• On the Relations between the Syntactic Theories of λμ-Calculi
• Parallel reduction in type free lambda/mu-calculus
• Proof assistants: history, ideas and future
• Proofs of strong normalisation for second order classical natural deduction
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The revised report on the syntactic theories of sequential control and state
• Typed Lambda Calculi and Applications

This page was built for publication: Adding Negation to Lambda Mu

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135761)