Extensional proofs in a propositional logic modulo isomorphisms
From MaRDI portal
Publication:6052705
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
isomorphismscut-eliminationlogicstrong normalizationsimply typed lambda calculuseta-expansionproof-reduction
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