Type-Based Termination with Sized Products

DOI10.1007/978-3-540-87531-4_35zbMath1156.68341OpenAlexW1602651206MaRDI QIDQ3540199

Colin Riba, Gilles Barthe, Benjamin Grégoire

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

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

Related Items (9)

Size-based termination of higher-order rewriting ⋮ Is sized typing for Coq practical? ⋮ Towards a practical library for monadic equational reasoning in Coq ⋮ A sound strategy to compile general recursion into finite depth pattern matching ⋮ Well-founded recursion with copatterns and sized types ⋮ Interactive programming in Agda – Objects and graphical user interfaces ⋮ Linear dependent types in a call-by-value scenario ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ Partiality and recursion in interactive theorem provers – an overview

Cites Work

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

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