Intensional harmony as isomorphism

DOI10.1007/978-3-031-50981-0_10MaRDI QIDQ6612873zbMATH OpenFDO

Authors Paolo Pistone, Luca Tranchini

Publication date 1 October 2024

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-50981-0_10

zbMATH Keywords

equivalence of derivationsidentity of proofsparametricityquantificationsecond-order logicsystem F

Mathematics Subject Classification ID

Proof theory and constructive mathematics (03Fxx)

Cites work

• A natural extension of natural deduction
• Axioms and decidability for type isomorphism in the presence of sums
• Deciding equivalence with sums and the empty type
• Die logizistische Grundlegung der Mathematik.
• Functorial polymorphism
• Fundamental concepts in programming languages
• scientific article; zbMATH DE number 3813515 (Why is no real title available?)
• scientific article; zbMATH DE number 3758289 (Why is no real title available?)
• scientific article; zbMATH DE number 3630747 (Why is no real title available?)
• scientific article; zbMATH DE number 1373518 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Identity of Proofs Based on Normalization and Generality
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• Open Problems in Proof-Theoretic Semantics
• Parametricity and variants of Girard's \(J\) operator
• Polymorphism and the obstinate circularity of second order logic: a victims' tale
• Proof, meaning and paradox: some remarks
• Proof-theoretic harmony: towards an intensional account
• Proof-theoretic semantics, paradoxes and the distinction between sense and denotation
• Stabilizing quantum disjunction
• The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony
• The category of finite sets and Cartesian closed categories
• The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus
• The naturality of natural deduction
• The system \({\mathcal F}\) of variable types, fifteen years later
• The Typed Böhm Theorem
• Truth from a proof-theoretic perspective
• λ-definable functionals andβη conversion

This page was built for publication: Intensional harmony as isomorphism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6612873)