Type-based termination of recursive definitions
From MaRDI portal
Publication:4463991
DOI10.1017/S0960129503004122zbMath1054.68027MaRDI QIDQ4463991
No author found.
Publication date: 27 May 2004
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
typed lambda calculus(co)inductive data types(co)recursive function definitionsCOQ systemtype-based proof assistant systems
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (24)
Unnamed Item ⋮ Size-based termination of higher-order rewriting ⋮ Mixed Inductive/Coinductive Types and Strong Normalization ⋮ Is sized typing for Coq practical? ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ A sound strategy to compile general recursion into finite depth pattern matching ⋮ Map fusion for nested datatypes in intensional type theory ⋮ Well-founded recursion with copatterns and sized types ⋮ Interactive programming in Agda – Objects and graphical user interfaces ⋮ Unnamed Item ⋮ Polarised subtyping for sized types ⋮ Type-based termination of generic programs ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ The Computability Path Ordering: The End of a Quest ⋮ Type-Based Termination with Sized Products ⋮ The Recursion Scheme from the Cofree Recursive Comonad ⋮ Termination checking with types ⋮ Compositional Coinduction with Sized Types ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ A Tutorial on Type-Based Termination ⋮ Using Structural Recursion for Corecursion ⋮ Implementing a normalizer using sized heterogeneous types ⋮ On the Relation between Sized-Types Based Termination and Semantic Labelling ⋮ Inductive and Coinductive Components of Corecursive Functions in Coq
Uses Software
This page was built for publication: Type-based termination of recursive definitions
