Remarks on isomorphisms of simple inductive types

DOI10.1016/S1571-0661(04)80760-6MaRDI QIDQ4924549zbMATH OpenOpenAlexFDO

Authors David Chemouil, Serguei V. Solov'ev

Publication date 6 June 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)80760-6

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Isomorphisms of simple inductive types through extensional rewriting
• Provable isomorphisms of types
• On isomorphisms of intersection types
• Toward isomorphism of intersection and union types
• Remarks on isomorphisms in typed lambda calculi with empty and sum types

Cites work

• Characterization of normal forms possessing inverse in the - --calculus
• scientific article; zbMATH DE number 1701346 (Why is no real title available?)
• scientific article; zbMATH DE number 4047065 (Why is no real title available?)
• scientific article; zbMATH DE number 3695144 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 733666 (Why is no real title available?)
• scientific article; zbMATH DE number 1405632 (Why is no real title available?)
• Inductive-data-type systems
• On the union of well-founded relations
• Provable isomorphisms of types
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(7)

• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• Isomorphisms of types in the presence of higher-order references
• A short survey of isomorphisms of types
• Isomorphisms of simple inductive types through extensional rewriting
• scientific article; zbMATH DE number 517016 (Why is no real title available?)
• scientific article; zbMATH DE number 6923849 (Why is no real title available?)
• Contextual isomorphisms

Describes a project that uses

Uses Software

• Coq
• Automath

This page was built for publication: Remarks on isomorphisms of simple inductive types

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