5 citations · 7 across the 6 of their papers we have counts for
5 papers · 1 filter
Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
Andrej Dudenhefner
Higher-order beta-matching is the following decision problem: given two simply typed lambda-terms, can the first term be instantiated to be beta-equivalent to the second term? This…
Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)
Andrej Dudenhefner
Semi-unification is the combination of first-order unification and first-order matching. The undecidability of semi-unification has been proven by Kfoury, Tiuryn, and Urzyczyn in t…
Mixin Composition Synthesis based on Intersection Types
Jan Bessai, Tzu-Chun Chen, Andrej Dudenhefner +3
We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over c…
Rank 3 Inhabitation of Intersection Types Revisited (Extended Version)
Andrej Dudenhefner, Jakob Rehof
We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we strengthen the previous result by showing that inte…
The Algebraic Intersection Type Unification Problem
Andrej Dudenhefner, Moritz Martens, Jakob Rehof
The algebraic intersection type unification problem is an important component in proof search related to several natural decision problems in intersection type systems. It is unkno…