On the Relation between Sized-Types Based Termination and Semantic Labelling

DOI10.1007/978-3-642-04027-6_13zbMath1257.68091OpenAlexW2070188769MaRDI QIDQ3644746

Cody Roux, Frédéric Blanqui

Publication date: 12 November 2009

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

Full work available at URL: https://hal.inria.fr/inria-00397689/file/main.pdf

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (3)

Size-based termination of higher-order rewriting ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ On the Relation between Sized-Types Based Termination and Semantic Labelling

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory reduction systems: Introduction and survey
• Dependent types for program termination verification
• Predictive Labeling
• On the Relation between Sized-Types Based Termination and Semantic Labelling
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• On the union of well-founded relations
• Type-based termination of recursive definitions
• Definitions by rewriting in the Calculus of Constructions
• Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
• Computer Science Logic
• Term Rewriting and Applications
• Semi-continuous Sized Types and Termination
• Rewriting Techniques and Applications

This page was built for publication: On the Relation between Sized-Types Based Termination and Semantic Labelling