The variable containment problem

DOI10.1007/3-540-61254-8_22MaRDI QIDQ4645807zbMATH OpenOpenAlexFDO

Authors Stefan Michael Kahrs

Publication date 11 January 2019

Published in Higher-Order Algebra, Logic, and Term Rewriting (Search for Journal in Brave)

Full work available at URL https://kar.kent.ac.uk/21244/1/varcont.pdf

zbMATH Keywords

abstract modelbase typeextra variablefree variablenormal form

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 2090083
• Higher Order   Matching is Undecidable
• Alpha-conversion and typability
• scientific article; zbMATH DE number 1405629
• Fundamentals of Computation Theory

Cites work

• Combinatory reduction systems: Introduction and survey
• Higher-order rewrite systems and their confluence
• scientific article; zbMATH DE number 2185671 (Why is no real title available?)
• scientific article; zbMATH DE number 2185672 (Why is no real title available?)
• scientific article; zbMATH DE number 431771 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 512783 (Why is no real title available?)
• scientific article; zbMATH DE number 516994 (Why is no real title available?)
• scientific article; zbMATH DE number 1984520 (Why is no real title available?)
• scientific article; zbMATH DE number 195199 (Why is no real title available?)
• Introduction to generalized type systems
• Modular aspects of properties of term rewriting systems related to normal forms
• Proving and applying program transformations expressed with second-order patterns
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The undecidability of the second-order unification problem
• Third order matching is decidable
• Towards a domain theory for termination proofs

Cited in

(5)

• Higher-order rewrite systems and their confluence
• Unary PCF is decidable
• Decidability of behavioural equivalence in unary PCF
• scientific article; zbMATH DE number 1405979 (Why is no real title available?)
• Infinitary rewriting: meta-theory and convergence

Describes a project that uses

Uses Software

• Automath

This page was built for publication: The variable containment problem

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