Type-Based Termination with Sized Products

DOI10.1007/978-3-540-87531-4_35zbMATH Open1156.68341OpenAlexW1602651206MaRDI QIDQ3540199FDOQ3540199

Authors: Gilles Barthe, Benjamin Grégoire, Colin Riba 

Publication date: 20 November 2008

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-87531-4_35

Recommendations

• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Semi-continuous Sized Types and Termination
• Semi-continuous Sized Types and Termination
• A Tutorial on Type-Based Termination
• Type-based termination of generic programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cites Work

• Higher-order subtyping
• Type-based termination of recursive definitions
• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
• Dependent types for program termination verification
• Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
• Typed Lambda Calculi and Applications
• Calculating sized types

Cited In (16)

• A Tutorial on Type-Based Termination
• Probabilistic termination by monadic affine sized typing
• On the Relation between Sized-Types Based Termination and Semantic Labelling
• Linear dependent types in a call-by-value scenario
• Size-based termination of higher-order rewriting
• Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
• Towards a practical library for monadic equational reasoning in Coq
• A sound strategy to compile general recursion into finite depth pattern matching
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Partiality and recursion in interactive theorem provers -- an overview
• Semi-continuous Sized Types and Termination
• Interactive programming in Agda -- objects and graphical user interfaces
• Semi-continuous Sized Types and Termination
• Type-based termination of generic programs
• Well-founded recursion with copatterns and sized types
• Is sized typing for Coq practical?

This page was built for publication: Type-Based Termination with Sized Products

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3540199)