Type-Based Termination with Sized Products

DOI10.1007/978-3-540-87531-4_35MaRDI QIDQ3540199zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(16)

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

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)