Provable isomorphisms of types

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)

zbMATH Keywords

Cartesian closed categorymodels of typed lambda calculus with surjective pairingpositive intuitionistic propositional logictypes as search keys in program libraries

Mathematics Subject Classification ID

Searching and sorting (68P10) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)

Related Items

Proof-functional connectives and realizability, Cartesian isomorphisms are symmetric monoidal: A justification of linear logic, Retrieving library functions by unifying types modulo linear isomorphism, Extensional proofs in a propositional logic modulo isomorphisms, On Isomorphisms of Intersection Types, On the unification problem for Cartesian closed categories, A confluent reduction for the λ-calculus with surjective pairing and terminal object, Genetic programming \(+\) proof search \(=\) automatic improvement, Remarks on Isomorphisms of Simple Inductive Types, Remarks on isomorphisms in typed lambda calculi with empty and sum types, Unnamed Item, Functional pearl: the distributive \(\lambda\)-calculus, Automorphisms of types in certain type theories and representation of finite groups, Efficient and flexible matching of recursive types, Isomorphism of intersection and union types, A coinductive completeness proof for the equivalence of recursive types

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