Proof normalisation in a logic identifying isomorphic propositions

DOI10.4230/LIPICS.FSCD.2019.14MaRDI QIDQ5089014FDO

Authors Alejandro Díaz-Caro, Gilles Dowek

Publication date 18 July 2022

Full work available at URL https://arxiv.org/abs/1501.06125

zbMATH Keywords

logicisomorphismscut-eliminationproof-reductionsimply typed \(\lambda\) calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Recommendations

• Isomorphic formulae in classical propositional logic
• Publication:4944850
• Formalized proof systems for propositional logic
• Identity of Proofs Based on Normalization and Generality
• scientific article; zbMATH DE number 65742

Cites work

• scientific article; zbMATH DE number 6712184 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 733666 (Why is no real title available?)
• scientific article; zbMATH DE number 7356679 (Why is no real title available?)
• A Filter Model for Concurrent $\lambda$-Calculus
• A System F accounting for scalars
• A relational semantics for parallelism and non-determinism in a functional setting
• A short survey of isomorphisms of types
• Homotopy type theory. Univalent foundations of mathematics
• Lambda-calculi for (strict) parallel functions
• Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
• Linearity in the non-deterministic call-by-value setting
• Linearity, non-determinism and solvability
• Mechanizing metatheory without typing contexts
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• On the expressive power of schemes
• Proof normalization modulo
• Provable isomorphisms of types
• Retrieving library identifiers via equational matching of types
• The algebraic lambda calculus
• The calculus of constructions
• The vectorial \(\lambda\)-calculus
• Theorem proving modulo

Cited in

(5)

• Functional pearl: the distributive \(\lambda\)-calculus
• A new connective in natural deduction, and its application to quantum computing
• A new connective in natural deduction, and its application to quantum computing
• Extensional proofs in a propositional logic modulo isomorphisms
• A quick overview on the quantum control approach to the lambda calculus

This page was built for publication: Proof normalisation in a logic identifying isomorphic propositions

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