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