Proofs, Upside Down
From MaRDI portal
Publication:2937799
DOI10.1007/978-3-319-03542-0_26zbMath1427.03034MaRDI QIDQ2937799
Publication date: 12 January 2015
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-03542-0_26
03F05: Cut-elimination and normal-form theorems
03B50: Many-valued logic
03F03: Proof theory in general (including proof-theoretic semantics)
03B20: Subsystems of classical logic (including intuitionistic logic)
03B40: Combinatory logic and lambda calculus
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A correspondence between type checking via reduction and type checking via evaluation
- On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
- Focusing and polarization in linear, intuitionistic, and classical logics
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Untersuchungen über das logische Schliessen. I
- A functional correspondence between call-by-need evaluators and lazy abstract machines
- A judgmental reconstruction of modal logic
- A Tutorial Implementation of a Dependently Typed Lambda Calculus
- Towards a Canonical Classical Natural Deduction System
- Completing Herbelin’s Programme
- The Zipper
- A Linear Spine Calculus
- Mechanizing Mathematical Reasoning