Type-based termination of recursive definitions
From MaRDI portal
(co)inductive data types(co)recursive function definitionsCOQ systemtype-based proof assistant systemstyped lambda calculus
Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)
Recommendations
- CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
- A Tutorial on Type-Based Termination
- Typed Lambda Calculi and Applications
- Termination checking with types
- On strong normalization of the calculus of constructions with type-based termination
Cited in
(32)- Inductively defined functions in functional programming languages
- Typed λ-calculus with recursive definitions
- scientific article; zbMATH DE number 1696606 (Why is no real title available?)
- A predicative analysis of structural recursion
- Inductive and coinductive components of corecursive functions in Coq
- Probabilistic termination by monadic affine sized typing
- Mixed Inductive/Coinductive Types and Strong Normalization
- Polarised subtyping for sized types
- The Computability Path Ordering: The End of a Quest
- Type-Based Termination with Sized Products
- Using Structural Recursion for Corecursion
- Implementing a normalizer using sized heterogeneous types
- On the Relation between Sized-Types Based Termination and Semantic Labelling
- Size-based termination of higher-order rewriting
- Termination checking with types
- On strong normalization of the calculus of constructions with type-based termination
- Efficient lambda encodings for Mendler-style coinductive types in Cedille
- The Recursion Scheme from the Cofree Recursive Comonad
- A Tutorial on Type-Based Termination
- scientific article; zbMATH DE number 7168147 (Why is no real title available?)
- Well-founded recursion with copatterns and sized types
- Interactive programming in Agda -- objects and graphical user interfaces
- Typed Lambda Calculi and Applications
- Compositional coinduction with sized types
- Partiality and recursion in interactive theorem provers -- an overview
- A user's friendly syntax to define recursive functions as typed λ-terms
- Is sized typing for Coq practical?
- A sound strategy to compile general recursion into finite depth pattern matching
- Map fusion for nested datatypes in intensional type theory
- Interpretations of recursively defined types
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- Type-based termination of generic programs
This page was built for publication: Type-based termination of recursive definitions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4463991)
