Type-based termination of generic programs

DOI10.1016/J.SCICO.2008.01.004MaRDI QIDQ923883zbMATH OpenOpenAlexFDO

Authors 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

functional programmingrecursionpolytypic programmingsized typetype-indexed type

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Towards Generic Programming with Sized Types
• Type-Based Termination with Sized Products
• Datatype-generic termination proofs
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Semi-continuous Sized Types and Termination

Cites work

• scientific article; zbMATH DE number 1223720 (Why is no real title available?)
• scientific article; zbMATH DE number 2100542 (Why is no real title available?)
• scientific article; zbMATH DE number 2111733 (Why is no real title available?)
• scientific article; zbMATH DE number 1424014 (Why is no real title available?)
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• A new approach to generic functional programming
• Computer Science Logic
• Flexible type analysis
• Generalizing generalized tries
• Generic Haskell: applications.
• Generic Programming
• Implementation of Functional Languages
• Intensional polymorphism in type-erasure semantics
• Iteration and coiteration schemes for higher-order and nested datatypes
• Mathematics of Program Construction
• Polytypic values possess polykinded types
• Programming Languages and Systems
• Semi-continuous Sized Types and Termination
• Towards Generic Programming with Sized Types
• Type-based termination of recursive definitions
• Type-indexed data types
• Typed Lambda Calculi and Applications
• Types and programing languages

Cited in

(9)

• Formal polytypic programs and proofs
• Type-Based Termination with Sized Products
• Towards Generic Programming with Sized Types
• Datatype-generic termination proofs
• Modular dependent induction in Coq, Mendler-style
• Logic Programming
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Semi-continuous Sized Types and Termination
• Dependent types for program termination verification

Describes a project that uses

Uses Software

• PolyLib
• Polyp
• AProVE
• Coq

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

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