Provable isomorphisms of types

DOI10.1017/S0960129500001444zbMATH Open0763.03011MaRDI QIDQ4017461FDOQ4017461

Authors: Kim B. Bruce, Roberto Di Cosmo, Giuseppe Longo 

Publication date: 16 January 1993

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Recommendations

• Second order isomorphic types: A proof theoretic study on second order \(\lambda\)-calculus with surjective pairing and terminal object
• Publication:4945229
• scientific article; zbMATH DE number 733666
• scientific article; zbMATH DE number 65742

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) Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Cites Work

• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• λ-definable functionals andβη conversion
• Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• The category of finite sets and Cartesian closed categories

Cited In (29)

• Title not available (Why is that?)
• Genetic programming \(+\) proof search \(=\) automatic improvement
• Automorphisms of types in certain type theories and representation of finite groups
• A coinductive completeness proof for the equivalence of recursive types
• On the unification problem for Cartesian closed categories
• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• Title not available (Why is that?)
• Isomorphisms of types in the presence of higher-order references
• A short survey of isomorphisms of types
• Retrieving library identifiers via equational matching of types
• Efficient and flexible matching of recursive types
• Title not available (Why is that?)
• Extensional proofs in a propositional logic modulo isomorphisms
• A confluent reduction for the λ-calculus with surjective pairing and terminal object
• Title not available (Why is that?)
• Retrieving library functions by unifying types modulo linear isomorphism
• Functional pearl: the distributive \(\lambda\)-calculus
• Title not available (Why is that?)
• Classical isomorphisms of types
• Isomorphisms of simple inductive types through extensional rewriting
• Proof-functional connectives and realizability
• Title not available (Why is that?)
• On Isomorphisms of Intersection Types
• Procedural isomorphism, analytic information and  -conversion by value
• Isomorphism of intersection and union types
• Using types as search keys in function libraries
• Remarks on isomorphisms of simple inductive types
• Cartesian isomorphisms are symmetric monoidal: A justification of linear logic
• Title not available (Why is that?)

This page was built for publication: Provable isomorphisms of types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4017461)