Proofs, Upside Down

DOI10.1007/978-3-319-03542-0_26zbMath1427.03034OpenAlexW2270243227MaRDI 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

Cut-elimination and normal-form theorems (03F05) Many-valued logic (03B50) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

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

This page was built for publication: Proofs, Upside Down