Denotational Semantics of the Simplified Lambda-Mu Calculus and a New Deduction System of Classical Type Theory
Classical (or Boolean) type theory is the type theory that allows the type inference (σ \to \bot) \to \bot => σ (the type counterpart of double-negation elimination), where σ is any type and \bot is absurdity type. This paper first presents a denotational semantics for a simplified version of Par...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-06-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1606.06385v1 |