Proof normalisation in a logic identifying isomorphic propositions

DOI10.4230/LIPICS.FSCD.2019.14MaRDI QIDQ5089014FDOQ5089014

Authors: Alejandro Díaz-Caro, Gilles Dowek 

Publication date: 18 July 2022

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

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

zbMATH Keywords

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

• Extensional proofs in a propositional logic modulo isomorphisms
• 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
• 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)