Termination checking with types
From MaRDI portal
Recommendations
- A Tutorial on Type-Based Termination
- Type-based termination of recursive definitions
- Typed Lambda Calculi and Applications
- On strong normalization of the calculus of constructions with type-based termination
- CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
Cites work
- A predicative analysis of structural recursion
- A syntactic approach to type soundness
- A theory of type polymorphism in programming
- A third-order representation of the -calculus
- An algorithm for type-checking dependent types
- Calculating sized types
- Dependent types for program termination verification
- Explaining Polymorphic Types
- scientific article; zbMATH DE number 1696606 (Why is no real title available?)
- scientific article; zbMATH DE number 4191621 (Why is no real title available?)
- scientific article; zbMATH DE number 4047683 (Why is no real title available?)
- scientific article; zbMATH DE number 4072437 (Why is no real title available?)
- scientific article; zbMATH DE number 1189292 (Why is no real title available?)
- scientific article; zbMATH DE number 1222571 (Why is no real title available?)
- scientific article; zbMATH DE number 1223720 (Why is no real title available?)
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- scientific article; zbMATH DE number 1343506 (Why is no real title available?)
- scientific article; zbMATH DE number 1956560 (Why is no real title available?)
- scientific article; zbMATH DE number 2061698 (Why is no real title available?)
- scientific article; zbMATH DE number 1543354 (Why is no real title available?)
- scientific article; zbMATH DE number 1765685 (Why is no real title available?)
- scientific article; zbMATH DE number 1385477 (Why is no real title available?)
- Inductive types and type constraints in the second-order lambda calculus
- Inductive-data-type systems
- Intersection types and computational effects
- Recursion and dynamic data-structures in bounded space: towards embedded ML programming
- Resource bound certification
- Rewriting Techniques and Applications
- Termination of nested and mutually recursive algorithms
- Termination of term rewriting using dependency pairs
- Tridirectional typechecking
- Type fixpoints, iteration vs. recursion
- Type-based termination of recursive definitions
- Types and programing languages
Cited in
(19)- A compact kernel for the calculus of inductive constructions
- Dependent types for program termination verification
- scientific article; zbMATH DE number 1696606 (Why is no real title available?)
- A predicative analysis of structural recursion
- Probabilistic termination by monadic affine sized typing
- The Computability Path Ordering: The End of a Quest
- Implementing a normalizer using sized heterogeneous types
- scientific article; zbMATH DE number 1330430 (Why is no real title available?)
- Type-based termination of recursive definitions
- Size-based termination of higher-order rewriting
- Heterogeneous substitution systems revisited
- On strong normalization of the calculus of constructions with type-based termination
- The Recursion Scheme from the Cofree Recursive Comonad
- A Tutorial on Type-Based Termination
- Logic Programming
- Typed Lambda Calculi and Applications
- T-rex: termination of recursive functions using lexicographic linear combinations
- Flow analysis of lazy higher-order functional programs
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
This page was built for publication: Termination checking with types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4659886)
