Paper Info
Title
On the unification of classical, intuitionistic and affine logics
Abstract
This article presents a unified logic that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the lambda mu calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.
Year
DOI
Venue
2019
10.1017/S0960129518000403
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
Field
DocType
Volume
Affine transformation,Discrete mathematics,Algebra,Unification,Mathematics
Journal
29
Issue
ISSN
Citations 
SP8
0960-1295
0
PageRank 
References 
Authors
0.34
8
1
Name
Order
Citations
PageRank
Chuck Liang11458.70