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 category; models of typed lambda calculus with surjective pairing; positive intuitionistic propositional logic; types as search keys in program libraries

Mathematics Subject Classification ID

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