Termination checking with types

DOI10.1051/ita:2004015zbMath1089.68028OpenAlexW2104860831MaRDI QIDQ4659886

Andreas Abel

Publication date: 21 March 2005

Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL: http://www.numdam.org/item?id=ITA_2004__38_4_277_0

zbMATH Keywords

inductive typesstrong normalizationsized typesbidirectional type checkingcourse-of-value recursionType-based termination

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Related Items (10)

Size-based termination of higher-order rewriting ⋮ Flow analysis of lazy higher-order functional programs ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ The Computability Path Ordering: The End of a Quest ⋮ The Recursion Scheme from the Cofree Recursive Comonad ⋮ A Tutorial on Type-Based Termination ⋮ Implementing a normalizer using sized heterogeneous types ⋮ Heterogeneous Substitution Systems Revisited ⋮ A compact kernel for the calculus of inductive constructions

Uses Software

• Coq
• ML
• Twelf
• LEGO

Cites Work

• A theory of type polymorphism in programming
• A syntactic approach to type soundness
• Termination of nested and mutually recursive algorithms
• Dependent types for program termination verification
• An algorithm for type-checking dependent types
• Termination of term rewriting using dependency pairs
• Inductive types and type constraints in the second-order lambda calculus
• A predicative analysis of structural recursion
• Recursion and dynamic data-structures in bounded space
• Type fixpoints
• A Third-Order Representation of the λμ-Calculus
• Intersection types and computational effects
• Explaining Polymorphic Types
• Tridirectional typechecking
• Type-based termination of recursive definitions
• Resource bound certification
• Rewriting Techniques and Applications
• Inductive-data-type systems
• Calculating sized types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Termination checking with types