Isomorphisms of simple inductive types through extensional rewriting

DOI10.1017/S0960129505004950MaRDI QIDQ3372685zbMATH OpenFDO

Authors David Chemouil

Publication date 10 March 2006

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

zbMATH Keywords

confluenceisomorphismsstrong normalisationinductive typesconversion rulesextensional simply typed \(\lambda\)-calculusfaithful copy

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Remarks on isomorphisms of simple inductive types
• Extensional Rewriting with Sums
• scientific article; zbMATH DE number 2182487
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• Provable isomorphisms of types

Cited in

(6)

• Remarks on isomorphisms of simple inductive types
• Isomorphisms of types in the presence of higher-order references
• A short survey of isomorphisms of types
• An insertion operator preserving infinite reduction sequences
• Conditionally reversible computations and weak universality in category theory
• scientific article; zbMATH DE number 733666 (Why is no real title available?)

This page was built for publication: Isomorphisms of simple inductive types through extensional rewriting

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