Third-order matching in the polymorphic lambda calculus

DOI10.1007/3-540-61254-8_28MaRDI QIDQ4645813zbMATH OpenOpenAlexFDO

Authors J. Springintveld

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://dspace.library.uu.nl/handle/1874/26340

zbMATH Keywords

finite ordermatch problemobject variablepolymorphic variabletype variable

Mathematics Subject Classification ID

Higher-order logic (03B16) Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 2185677
• Third order matching is decidable
• Decidability of fourth-order matching
• scientific article; zbMATH DE number 1223619
• Computer Science Logic

Cites work

• Embedding first order predicate logic in fragments of intuitionistic logic
• scientific article; zbMATH DE number 2185671 (Why is no real title available?)
• scientific article; zbMATH DE number 2185677 (Why is no real title available?)
• scientific article; zbMATH DE number 29189 (Why is no real title available?)
• scientific article; zbMATH DE number 42964 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 176135 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• The calculus of constructions
• The Clausal Theory of Types
• The undecidability of pattern matching in calculi where primitive recursive functions are representable
• Third order matching is decidable
• Unification under a mixed prefix

Cited in

(6)

• Third order matching is decidable
• scientific article; zbMATH DE number 2185677 (Why is no real title available?)
• scientific article; zbMATH DE number 29189 (Why is no real title available?)
• scientific article; zbMATH DE number 1223619 (Why is no real title available?)
• scientific article; zbMATH DE number 626035 (Why is no real title available?)
• scientific article; zbMATH DE number 2043532 (Why is no real title available?)

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Third-order matching in the polymorphic lambda calculus

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