Intuitionistic Letcc via Labelled Deduction
From MaRDI portal
Publication:4982116
DOI10.1016/j.entcs.2009.02.031zbMath1347.03061OpenAlexW2051358061MaRDI QIDQ4982116
Publication date: 23 March 2015
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2009.02.031
Modal logic (including the logic of norms) (03B45) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Intuitionistic and classical natural deduction systems with the catch and the throw rules
- Natural deduction for non-classical logics
- T-string unification: Unifying prefixes in non-classical proof methods
- A Formulae-as-Types Interpretation of Subtractive Logic
- A confluent λ-calculus with a catch/throw mechanism
- Call-by-value is dual to call-by-name
- Typed Lambda Calculi and Applications
- Some theorems about the sentential calculi of Lewis and Heyting