Strong Normalization and Equi-(Co)Inductive Types

e type system for the l—m˜d—E™—l™ulus enri™hed with re™urE sive —nd ™ore™ursive fun™tions over equiEindu™tive —nd E™oindu™tive types is presented in whi™h —ll wellEtyped progr—ms —re strongly norm—lizingF „he ™hoi™e of equiEindu™tive typesD inste—d of the more ™ommon isoE indu™tive typesD in)uen™es ˜oth redu™tion rules —nd the strong norm—lE iz—tion proofF fy em˜edding isoE into equiEtypesD the l—tter ones —re re™ognized —s more fund—ment—lF e model ˜—sed on orthogon—lity is ™onE stru™ted where — sem—nti™—l type ™orresponds to — set of o˜serv—tionsD —nd soundness of the type system is provenF

• Type: Conference
• Year: 2007
• Where: TLCA
• Authors: Andreas Abel
• Keywords: EquiEindu™tive TypesD Inste—d, Sem—nti™—l Type ™orresponds, Theoretical Computer Science, TLCA 2007, —nd ™ore™ursive Fun™tions