Proofs, Upside Down

DOI10.1007/978-3-319-03542-0_26zbMath1427.03034MaRDI QIDQ2937799

Matthias Puech

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

Mathematics Subject Classification ID

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