8 Search Results for "Urzyczyn, Pawel"

Document
DOI: 10.4230/LIPIcs.TIME.2025.5
Higher-Order Timed Automata and Tail Recursion

Authors: Florian Bruse

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Abstract
Timed Automata (TA) are a popular formalism to model systems in dense linear time. However, due to their finite state-space, they can only model systems with a finitary logical behavior. There are extensions to e.g., timed pushdown systems and timed recursive state machines. Higher-Order Recursion Schemes (HORS) are another popular model for infinite-state, non-regular systems, naturally stratified by their type-theoretic order. We recently introduced Real-Time Recursion schemes as an approximation of HORS to real-time systems. This paper updates Real-Time Recursion Schemes into Higher-Order Timed Automata, a formalism that defines a tree-shaped timed automaton, which is more suitable to model actual systems. We show that the model-checking problem against the timed version of the modal mu-calculus exhibits the expected complexity bounds, i.e., an increase by one exponential towards the untimed version. We also show that, in the presence of tail recursion, half an exponential can be recovered, mirroring similar gains in the untimed setting. We also give a matching lower bound for the special case of order-1 HORTA. We conjecture that this can be generalized for all orders.
Cite as

Florian Bruse. Higher-Order Timed Automata and Tail Recursion. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruse:LIPIcs.TIME.2025.5,
  author =	{Bruse, Florian},
  title =	{{Higher-Order Timed Automata and Tail Recursion}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.5},
  URN =		{urn:nbn:de:0030-drops-244519},
  doi =		{10.4230/LIPIcs.TIME.2025.5},
  annote =	{Keywords: Timed Automata, Higher-Order Recursion Schemes, Tree Automata, Tail Recursion}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.17
Mechanized Undecidability of Higher-Order Beta-Matching

Authors: Andrej Dudenhefner

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Higher-order β-matching is the following decision problem: given two simply typed λ-terms, can the first term be instantiated to be β-equivalent to the second term? This problem was formulated by Huet in the 1970s and shown undecidable by Loader in 2003 by reduction from λ-definability. The present work provides a novel undecidability proof for higher-order β-matching, in an effort to verify this result by means of a proof assistant. Rather than starting from λ-definability, the presented proof encodes a restricted form of string rewriting as higher-order β-matching. The particular approach is similar to Urzyczyn’s undecidability result for intersection type inhabitation. The presented approach has several advantages. First, the proof is simpler to verify in full detail due to the simple form of rewriting systems, which serve as a starting point. Second, undecidability of the considered problem in string rewriting is already certified using the Coq proof assistant. As a consequence, we obtain a certified many-one reduction from the Halting Problem to higher-order β-matching. Third, the presented approach identifies a uniform construction which shows undecidability of higher-order β-matching, λ-definability, and intersection type inhabitation. The presented undecidability proof is mechanized in the Coq proof assistant and contributed to the existing Coq Library of Undecidability Proofs.
Cite as

Andrej Dudenhefner. Mechanized Undecidability of Higher-Order Beta-Matching. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dudenhefner:LIPIcs.FSCD.2025.17,
  author =	{Dudenhefner, Andrej},
  title =	{{Mechanized Undecidability of Higher-Order Beta-Matching}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{17:1--17:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.17},
  URN =		{urn:nbn:de:0030-drops-236323},
  doi =		{10.4230/LIPIcs.FSCD.2025.17},
  annote =	{Keywords: lambda-calculus, simple types, undecidability, higher-order matching, mechanization, Coq}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.18
Constructive Many-One Reduction from the Halting Problem to Semi-Unification

Authors: Andrej Dudenhefner

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
The undecidability of semi-unification (unification combined with matching) has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s. The original argument is by Turing reduction from Turing machine immortality (existence of a diverging configuration). There are several aspects of the existing work which can be improved upon. First, many-one completeness of semi-unification is not established due to the use of Turing reductions. Second, existing mechanizations do not cover a comprehensive reduction from Turing machine halting to semi-unification. Third, reliance on principles such as König’s lemma or the fan theorem does not support constructivity of the arguments. Improving upon the above aspects, the present work gives a constructive many-one reduction from the Turing machine halting problem to semi-unification. This establishes many-one completeness of semi-unification. Computability of the reduction function, constructivity of the argument, and correctness of the argument is witnessed by an axiom-free mechanization in the Coq proof assistant. The mechanization is incorporated into the existing Coq library of undecidability proofs. Notably, the mechanization relies on a technique invented by Hooper in the 1960s for Turing machine immortality. An immediate consequence of the present work is an alternative approach to the constructive many-one equivalence of System F typability and System F type checking, compared to the argument established in the 1990s by Wells.
Cite as

Andrej Dudenhefner. Constructive Many-One Reduction from the Halting Problem to Semi-Unification. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dudenhefner:LIPIcs.CSL.2022.18,
  author =	{Dudenhefner, Andrej},
  title =	{{Constructive Many-One Reduction from the Halting Problem to Semi-Unification}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{18:1--18:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.18},
  URN =		{urn:nbn:de:0030-drops-157380},
  doi =		{10.4230/LIPIcs.CSL.2022.18},
  annote =	{Keywords: constructive mathematics, undecidability, mechanization, semi-unification}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.11
Duality in Intuitionistic Propositional Logic

Authors: Paweł Urzyczyn

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
It is known that provability in propositional intuitionistic logic is Pspace-complete. As Pspace is closed under complements, there must exist a Logspace-reduction from refutability to provability. Here we describe a direct translation: given a formula φ, we define ̅φ so that ̅φ is provable if and only if φ is not.
Cite as

Paweł Urzyczyn. Duality in Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 11:1-11:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{urzyczyn:LIPIcs.TYPES.2020.11,
  author =	{Urzyczyn, Pawe{\l}},
  title =	{{Duality in Intuitionistic Propositional Logic}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{11:1--11:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.11},
  URN =		{urn:nbn:de:0030-drops-138901},
  doi =		{10.4230/LIPIcs.TYPES.2020.11},
  annote =	{Keywords: Intuitionistic logic, Complexity}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.3
Deconfined Intersection Types in Java

Authors: Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
We show how Java intersection types can be freed from their confinement in type casts, in such a way that the proposed Java extension is safe and fully compatible with the current language. To this aim, we exploit two calculi which formalise the simple Java core and the extended language, respectively. Namely, the second calculus extends the first one by allowing an intersection type to be used anywhere in place of a nominal type. We define a translation algorithm, compiling programs of the extended language into programs of the former calculus. The key point is the interaction between λ-expressions and intersection types, that adds safe expressiveness while being the crucial matter in the translation. We prove that the translation preserves typing and semantics. Thus, typed programs in the proposed extension are translated to typed Java programs. Moreover, semantics of translated programs coincides with the one of the source programs.
Cite as

Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Deconfined Intersection Types in Java. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dezaniciancaglini_et_al:OASIcs.Gabbrielli.3,
  author =	{Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Venneri, Betti},
  title =	{{Deconfined Intersection Types in Java}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{3:1--3:25},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.3},
  URN =		{urn:nbn:de:0030-drops-132256},
  doi =		{10.4230/OASIcs.Gabbrielli.3},
  annote =	{Keywords: Intersection Types, Featherweight Java, Lambda Expressions}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.2
A Simpler Undecidability Proof for System F Inhabitation

Authors: Andrej Dudenhefner and Jakob Rehof

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
Provability in the intuitionistic second-order propositional logic (resp. inhabitation in the polymorphic lambda-calculus) was shown by Löb to be undecidable in 1976. Since the original proof is heavily condensed, Arts in collaboration with Dekkers provided a fully unfolded argument in 1992 spanning approximately fifty pages. Later in 1997, Urzyczyn developed a different, syntax oriented proof. Each of the above approaches embeds (an undecidable fragment of) first-order predicate logic into second-order propositional logic. In this work, we develop a simpler undecidability proof by reduction from solvability of Diophantine equations (is there an integer solution to P(x_1, ..., x_n) = 0 where P is a polynomial with integer coefficients?). Compared to the previous approaches, the given reduction is more accessible for formalization and more comprehensible for didactic purposes. Additionally, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of "type theory inside type theory".
Cite as

Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 2:1-2:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2018.2,
  author =	{Dudenhefner, Andrej and Rehof, Jakob},
  title =	{{A Simpler Undecidability Proof for System F Inhabitation}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{2:1--2:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.2},
  URN =		{urn:nbn:de:0030-drops-114061},
  doi =		{10.4230/LIPIcs.TYPES.2018.2},
  annote =	{Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.251
Restricted Positive Quantification Is Not Elementary

Authors: Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
We show that a restricted variant of constructive predicate logic with positive (covariant) quantification is of super-elementary complexity. The restriction is to limit the number of eigenvariables used in quantifier introductions rules to a reasonably usable level. This construction suggests that the known non-elementary decision algorithms for positive logic may actually be best possible.
Cite as

Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz. Restricted Positive Quantification Is Not Elementary. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 251-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schubert_et_al:LIPIcs.TYPES.2014.251,
  author =	{Schubert, Aleksy and Urzyczyn, Pawel and Walukiewicz-Chrzaszcz, Daria},
  title =	{{Restricted Positive Quantification Is Not Elementary}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{251--273},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.251},
  URN =		{urn:nbn:de:0030-drops-55002},
  doi =		{10.4230/LIPIcs.TYPES.2014.251},
  annote =	{Keywords: constructive logic, complexity, automata theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.243
Bounded Combinatory Logic

Authors: Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
In combinatory logic one usually assumes a fixed set of basic combinators (axiom schemes), usually K and S. In this setting the set of provable formulas (inhabited types) is PSPACE-complete in simple types and undecidable in intersection types. When arbitrary sets of axiom schemes are considered, the inhabitation problem is undecidable even in simple types (this is known as Linial-Post theorem). k-bounded combinatory logic with intersection types arises from combinatory logic by imposing the bound k on the depth of types (formulae) which may be substituted for type variables in axiom schemes. We consider the inhabitation (provability) problem for k-bounded combinatory logic: Given an arbitrary set of typed combinators and a type tau, is there a combinatory term of type tau in k-bounded combinatory logic? Our main result is that the problem is (k+2)-EXPTIME complete for k-bounded combinatory logic with intersection types, for every fixed k (and hence non-elementary when k is a parameter). We also show that the problem is EXPTIME-complete for simple types, for all k. Theoretically, our results give new insight into the expressive power of intersection types. From an application perspective, our results are useful as a foundation for composition synthesis based on combinatory logic.
Cite as

Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn. Bounded Combinatory Logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 243-258, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{dudder_et_al:LIPIcs.CSL.2012.243,
  author =	{D\"{u}dder, Boris and Martens, Moritz and Rehof, Jakob and Urzyczyn, Pawel},
  title =	{{Bounded Combinatory Logic}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{243--258},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.243},
  URN =		{urn:nbn:de:0030-drops-36763},
  doi =		{10.4230/LIPIcs.CSL.2012.243},
  annote =	{Keywords: Intersection types, Inhabitation, Composition synthesis}
}
  • Refine by Type
  • 8 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2022
  • 1 2021
  • 1 2020
  • 1 2019
  • Show More...

  • Refine by Author
  • 3 Dudenhefner, Andrej
  • 2 Rehof, Jakob
  • 2 Urzyczyn, Pawel
  • 1 Bruse, Florian
  • 1 Dezani-Ciancaglini, Mariangiola
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Computability
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Lambda calculus
  • Show More...

  • Refine by Keyword
  • 2 Coq
  • 2 Inhabitation
  • 2 mechanization
  • 2 undecidability
  • 1 Complexity
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact