Polymorphic higher-order termination

DOI10.4230/LIPICS.FSCD.2019.12MaRDI QIDQ5089012zbMATH OpenFDO

Authors Łukasz Czajka, Cynthia Kop

Publication date 18 July 2022

Full work available at URL https://arxiv.org/abs/1904.09859

zbMATH Keywords

polymorphismterminationhigher-order rewritingpermutative conversions

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Recommendations

• Polynomial interpretations for higher-order rewriting
• Polymorphic higher-order recursive path orderings
• Normal higher-order termination
• A termination ordering for higher order rewrite systems
• scientific article; zbMATH DE number 2185672

Cites work

• scientific article; zbMATH DE number 2185672 (Why is no real title available?)
• scientific article; zbMATH DE number 996558 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 7204561 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• A syntactic embedding of predicate logic into second-order propositional logic
• An introduction to (co)algebra and (co)induction
• Definitions by rewriting in the Calculus of Constructions
• Dynamic dependency pairs for algebraic functional systems
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Introduction to bisimulation and coinduction
• Lectures on the Curry-Howard isomorphism
• Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
• Polymorphic higher-order recursive path orderings
• Polymorphic rewrite rules: confluence, type inference, and instance validation
• Polynomial interpretations for higher-order rewriting
• Practical coinduction
• Short Proofs of Strong Normalization
• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• Termination of rewriting in the Calculus of Constructions

Cited in

(1)

• scientific article; zbMATH DE number 7566074 (Why is no real title available?)

This page was built for publication: Polymorphic higher-order termination

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