Provable isomorphisms of types
From MaRDI portal
Publication:4017461
DOI10.1017/S0960129500001444zbMath0763.03011MaRDI QIDQ4017461
Kim B. Bruce, Roberto Di Cosmo
Publication date: 16 January 1993
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Cartesian closed category; models of typed lambda calculus with surjective pairing; positive intuitionistic propositional logic; types as search keys in program libraries
68P10: Searching and sorting
18D15: Closed categories (closed monoidal and Cartesian closed categories, etc.)
03B40: Combinatory logic and lambda calculus
Related Items
Retrieving library functions by unifying types modulo linear isomorphism, On the unification problem for Cartesian closed categories, A confluent reduction for the λ-calculus with surjective pairing and terminal object, Remarks on Isomorphisms of Simple Inductive Types, Unnamed Item, Isomorphism of intersection and union types, Extensional proofs in a propositional logic modulo isomorphisms, Genetic programming \(+\) proof search \(=\) automatic improvement, Proof-functional connectives and realizability, A coinductive completeness proof for the equivalence of recursive types, Efficient and flexible matching of recursive types, Functional pearl: the distributive \(\lambda\)-calculus, Remarks on isomorphisms in typed lambda calculi with empty and sum types, Automorphisms of types in certain type theories and representation of finite groups, On Isomorphisms of Intersection Types, Cartesian isomorphisms are symmetric monoidal: A justification of linear logic
Cites Work
- Unnamed Item
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
- Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
- The category of finite sets and Cartesian closed categories
- λ-definable functionals andβη conversion