Zobrazeno 1 - 10
of 31
pro vyhledávání: '"Andrej Dudenhefner"'
Autor:
Andrej Dudenhefner
Publikováno v:
Logical Methods in Computer Science, Vol Volume 19, Issue 4 (2023)
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 (existenc
Externí odkaz:
https://doaj.org/article/cae125669d774f50a7f1da230ae9db6c
Publikováno v:
Logical Methods in Computer Science, Vol Volume 14, Issue 1 (2018)
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. Inte
Externí odkaz:
https://doaj.org/article/a66a1daef1a248fe9a0629b712ed9b85
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 177, Iss Proc. ITRS 2014, Pp 79-93 (2015)
We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally represent mixins
Externí odkaz:
https://doaj.org/article/dcfc56705adf4c97b44b686c6221480d
Autor:
Andrej Dudenhefner, Paweł Urzyczyn
Publikováno v:
ACM Transactions on Computational Logic. 22:1-16
We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced
Publikováno v:
Logical Methods in Computer Science, Vol Volume 13, Issue 3 (2017)
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 unificatio
Externí odkaz:
https://doaj.org/article/f707db9efd1f4096abc5f54281676aaa
Autor:
Andrej Dudenhefner
Publikováno v:
LICS
The undecidability of both typability and type checking for System F (polymorphic lambda-calculus) was established by Wells in the 1990s. For type checking Wells gave an astonishingly simple reduction from semi-unification (first-order unification co
Autor:
Andrej Dudenhefner, Jakob Rehof
Publikováno v:
Fundamenta Informaticae. 170:93-110
We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we simplify the existing proof, reducing simple semi-Thue systems to intersection type inhabitation in the original Coppo-De
Autor:
Andrej Dudenhefner, Jakob Rehof
We develop an algebraic and algorithmic theory of principality for the recently introduced framework of intersection type calculi with dimensional bound. The theory enables inference of principal type information under dimensional bound, it provides
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3e9dffbe1f511352b19ef7dbf7083522
https://publica.fraunhofer.de/handle/publica/260848
https://publica.fraunhofer.de/handle/publica/260848
Autor:
Andrej Dudenhefner, Jakob Rehof
Publikováno v:
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
Autor:
Andrej Dudenhefner, Jakob Rehof
Publikováno v:
POPL
A notion of dimension in intersection typed λ-calculi is presented. The dimension of a typed λ-term is given by the minimal norm of an elaboration (a proof theoretic decoration) necessary for typing the term at its type, and, intuitively, measures