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)

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)

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

Cites work

• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• 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
• The lambda calculus. Its syntax and semantics. Rev. ed.
• λ-definable functionals andβη conversion

Cited in

(31)

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

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)