Inductive, coinductive, and pointed types

DOI10.1145/232627.232640MaRDI QIDQ2817688zbMATH OpenOpenAlexFDO

Authors Brian T. Howard

Publication date 1 September 2016

Published in Proceedings of the first ACM SIGPLAN international conference on Functional programming - ICFP '96 (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.84.1416

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 4047683
• General Recursion via Coinductive Types
• Two extensions of System F with (co)iteration and primitive (co)recursion principles
• scientific article; zbMATH DE number 1342222
• Type theory based on dependent inductive and coinductive types

Cited in

(12)

• Undecidability of equality for codata types
• Formal derivation of greedy algorithms from relational specifications: a tutorial
• Refining inductive types
• Global semantic typing for inductive and coinductive computing
• When Is a Type Refinement an Inductive Type?
• Two extensions of System F with (co)iteration and primitive (co)recursion principles
• scientific article; zbMATH DE number 1342222 (Why is no real title available?)
• scientific article; zbMATH DE number 2003163 (Why is no real title available?)
• Type theory based on dependent inductive and coinductive types
• Induction by coinduction and control operators in call-by-name
• Builtin types viewed as inductive families
• Call-by-push-value: Decomposing call-by-value and call-by-name

This page was built for publication: Inductive, coinductive, and pointed types

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