Search

• < Previous
• 1
• Next >

---

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 unknown and remains open whether the algebraic intersection type unification problem is decidable. We give the first&nbsp;[&hellip;]

---

Mixin Composition Synthesis based on Intersection Types

Jan Bessai ; Tzu-Chun Chen ; Andrej Dudenhefner ; Boris Düdder ; Ugo de'Liguoro ; Jakob Rehof.

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 classes, are expressed as terms in a lambda calculus with records. Intersection types with records and record-merge are&nbsp;[&hellip;]

---

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 the 1990s by Turing reduction from Turing machine immortality (existence of a diverging configuration). The particular&nbsp;[&hellip;]

---