Extensional proofs in a propositional logic modulo isomorphisms

DOI10.1016/j.tcs.2023.114172arXiv2002.03762OpenAlexW3005285175MaRDI QIDQ6052705

Alejandro Díaz-Caro, Gilles Dowek

Publication date: 17 October 2023

Published in: Theoretical Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

isomorphismscut-eliminationlogicstrong normalizationsimply typed lambda calculuseta-expansionproof-reduction

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A relational semantics for parallelism and non-determinism in a functional setting
• The vectorial \(\lambda\)-calculus
• The calculus of constructions
• A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem
• Lambda-calculi for (strict) parallel functions
• An equivalence between lambda- terms
• Theorem proving modulo
• The category of finite sets and Cartesian closed categories
• Mechanizing metatheory without typing contexts
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• A System F accounting for scalars
• Linearity in the Non-deterministic Call-by-Value Setting
• Linearity, Non-determinism and Solvability
• A short survey of isomorphisms of types
• Classical isomorphisms of types
• Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
• The algebraic lambda calculus
• Provable isomorphisms of types
• A Filter Model for Concurrent $\lambda$-Calculus
• Simulating expansions without expansions
• Proof normalization modulo
• The virtues of eta-expansion
• Typing Quantum Superpositions and Measurement
• Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative
• Efficient algorithms for isomorphisms of simple types

This page was built for publication: Extensional proofs in a propositional logic modulo isomorphisms