Third-order matching in the polymorphic lambda calculus

DOI10.1007/3-540-61254-8_28zbMath1434.03061OpenAlexW2113723828MaRDI QIDQ4645813

Jan 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

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

Uses Software

• Automath

Cites Work

• The calculus of constructions
• Unification under a mixed prefix
• The undecidability of pattern matching in calculi where primitive recursive functions are representable
• Third order matching is decidable
• Embedding first order predicate logic in fragments of intuitionistic logic
• The Clausal Theory of Types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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