Type-based termination of generic programs

DOI10.1016/j.scico.2008.01.004zbMath1192.68134OpenAlexW2158523001MaRDI QIDQ923883

Andreas Abel

Publication date: 24 July 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2008.01.004

zbMATH Keywords

recursionfunctional programmingpolytypic programmingsized typetype-indexed type

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (3)

Unnamed Item ⋮ Formal polytypic programs and proofs ⋮ Modular Dependent Induction in Coq, Mendler-Style

Uses Software

• Coq
• AProVE
• Polyp
• PolyLib

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Polytypic values possess polykinded types
• Iteration and coiteration schemes for higher-order and nested datatypes
• Type-indexed data types
• Flexible type analysis
• Towards Generic Programming with Sized Types
• Type-based termination of recursive definitions
• Generalizing generalized tries
• Intensional polymorphism in type-erasure semantics
• A new approach to generic functional programming
• Generic Programming
• Generic Programming
• Mathematics of Program Construction
• Computer Science Logic
• Implementation of Functional Languages
• Programming Languages and Systems
• Typed Lambda Calculi and Applications
• Semi-continuous Sized Types and Termination

This page was built for publication: Type-based termination of generic programs