Isomorphisms of simple inductive types through extensional rewriting

DOI10.1017/S0960129505004950zbMATH Open1096.03009MaRDI QIDQ3372685FDOQ3372685

Authors: David Chemouil 

Publication date: 10 March 2006

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

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

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)

Cited In (6)

• Conditionally reversible computations and weak universality in category theory
• Isomorphisms of types in the presence of higher-order references
• A short survey of isomorphisms of types
• An insertion operator preserving infinite reduction sequences
• Title not available (Why is that?)
• Remarks on isomorphisms of simple inductive types

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)