Algorithmic triviality of abstract structures. - Pawel Urzyczyn (Fundam. Informaticae, 1981)

The Unwind Property in Certain Algebras - Pawel Urzyczyn (Inf. Control., 1981)

Deterministic Context-Free Dynamic Logic is More Expressive than Deterministic Dynamic Logic of Regular Programs. - Pawel Urzyczyn (FCT, 1983)

Some Relationships between Logics of Programs and Complexity Theory (Extended Abstract) - Jerzy Tiuryn; Pawel Urzyczyn (FOCS, 1983)

Necessary and Sufficient Conditions for University of Programming Formalisms (Partial Report). - A. J. Kfoury; Pawel Urzyczyn (Logic of Programs, 1983)

Nontrivial Definability by Flow-Chart Programs - Pawel Urzyczyn (Inf. Control., 1983)

A Necessary and Sufficient Condition in Order That a Herbrand Interpretation Be Expressive Relative to Recursive Programs - Pawel Urzyczyn (Inf. Control., 1983)

Remarks on Comparing Expressive Power of Logics of Programs. - Jerzy Tiuryn; Pawel Urzyczyn (MFCS, 1984)

Necessary and Sufficient Conditions for the Universality of Programming Formalisms. - A. J. Kfoury; Pawel Urzyczyn (Acta Informatica, 1985)

"During" Cannot be Expressed by "After". - Pawel Urzyczyn (J. Comput. Syst. Sci., 1986)

Verification of Programs with Higher-Order Arrays. - Wojciech Kowalczyk; Pawel Urzyczyn (FCT, 1987)

The Hierarchy of Finitely Typed Functional Programs (Short Version) - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (LICS, 1987)

On the Computational Power of Universally Polymorphic Recursion - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (LICS, 1988)

A Proper Extension of ML with an Effective Type-Assignment. - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (POPL, 1988)

Some Relationships Between Logics of Programs and Complexity Theory. - Jerzy Tiuryn; Pawel Urzyczyn (Theor. Comput. Sci., 1988)

Algo-Like Languages with Higher-Order Procedures and Their Expressive Power. - A. J. Kfoury; Pawel Urzyczyn (Logic at Botik, 1989)

Computational Consequences and Partial Solutions of a Generalized Unification Problem (Partial Report) - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (LICS, 1989)

ML Typability is DEXTIME-Complete. - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (CAAP, 1990)

The Undecidability of the Semi-Unification Problem (Preliminary Report) - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (STOC, 1990)

On the Expressive Power of Finitely and Universally Polymorphic Recursive Procedures. - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (Theor. Comput. Sci., 1992)

Type reconstruction in F-omega is undecidable. - Pawel Urzyczyn (TLCA, 1993)

Primitive Recursion with Extential Types. - Pawel Urzyczyn (Fundam. Informaticae, 1993)

Type Reconstruction in the Presence of Polymorphic Recursion. - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (ACM Trans. Program. Lang. Syst., 1993)

The Undecidability of the Semi-unification Problem - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (Inf. Comput., 1993)

Comparing Cubes. - Steffen van Bakel; Luigi Liquori; Simona Ronchi Della Rocca; Pawel Urzyczyn (LFCS, 1994)

An Analysis of ML Typability. - A. J. Kfoury; Jerzy Tiuryn; Pawel Urzyczyn (J. ACM, 1994)

Positive Recursive Type Assignment. - Pawel Urzyczyn (Fundam. Informaticae, 1996)

Discrimination by Parallel Observers. - Mariangiola Dezani-Ciancaglini; Jerzy Tiuryn; Pawel Urzyczyn (LICS, 1997)

Inhabitation in Typed Lambda-Calculi (A Syntactic Approach). - Pawel Urzyczyn (TLCA, 1997)

Comparing Cubes of Typed and Type Assignment Systems. - Steffen van Bakel; Luigi Liquori; Simona Ronchi Della Rocca; Pawel Urzyczyn (Ann. Pure Appl. Log., 1997)

Type Reconstruction in Fomega. - Pawel Urzyczyn (Math. Struct. Comput. Sci., 1997)

Type Fixpoints: Iteration vs. Recursion. - Zdzislaw Splawski; Pawel Urzyczyn (ICFP, 1999)

Discrimination by Parallel Observers: The Algorithm. - Mariangiola Dezani-Ciancaglini; Jerzy Tiuryn; Pawel Urzyczyn (Inf. Comput., 1999)

Alpha-Conversion and Typability. - A. J. Kfoury; Simona Ronchi Della Rocca; Jerzy Tiuryn; Pawel Urzyczyn (Inf. Comput., 1999)

The Emptiness Problem for Intersection Types. - Pawel Urzyczyn (J. Symb. Log., 1999)

Deciding Monadic Theories of Hyperalgebraic Trees. - Teodor Knapik; Damian Niwinski; Pawel Urzyczyn (TLCA, 2001)

Higher-Order Pushdown Trees Are Easy. - Teodor Knapik; Damian Niwinski; Pawel Urzyczyn (FoSSaCS, 2002)

Retractions of Types with Many Atoms - Laurent Regnier; Pawel Urzyczyn (CoRR, 2002)

The Subtyping Problem for Second-Order Types Is Undecidable. - Jerzy Tiuryn; Pawel Urzyczyn (Inf. Comput., 2002)

Type Inference for Nested Self Types. - Viviana Bono; Jerzy Tiuryn; Pawel Urzyczyn (TYPES, 2003)

A Simple Proof of the Undecidability of Strong Normalisation. - Pawel Urzyczyn (Math. Struct. Comput. Sci., 2003)

My (Un)Favourite Things. - Pawel Urzyczyn (CSL, 2004)

Unsafe Grammars and Panic Automata. - Teodor Knapik; Damian Niwinski; Pawel Urzyczyn; Igor Walukiewicz (ICALP, 2005)

Typed Lambda Calculi and Applications 2003, Selected Papers. - Martin Hofmann 001; Pawel Urzyczyn (Fundam. Informaticae, 2005)

In the Search of a Naive Type Theory. - Agnieszka Kozubek; Pawel Urzyczyn (TYPES, 2007)

Strong cut-elimination in sequent calculus using Klop's iota-translation and perpetual reductions. - Morten Heine Sørensen; Pawel Urzyczyn (J. Symb. Log., 2008)

Inhabitation of Low-Rank Intersection Types. - Pawel Urzyczyn (TLCA, 2009)

Preface. - Anna Gambin; Damian Niwinski; Pawel Urzyczyn (Fundam. Informaticae, 2010)

The Logic of Persistent Intersection. - Pawel Urzyczyn (Fundam. Informaticae, 2010)

A Syntactic Embedding of Predicate Logic into Second-Order Propositional Logic. - Morten Heine Sørensen; Pawel Urzyczyn (Notre Dame J. Formal Log., 2010)

Finite Combinatory Logic with Intersection Types. - Jakob Rehof; Pawel Urzyczyn (TLCA, 2011)

The Complexity of Inhabitation with Explicit Intersection. - Jakob Rehof; Pawel Urzyczyn (Logic and Program Semantics, 2012)

Bounded Combinatory Logic. - Boris Düdder; Moritz Martens; Jakob Rehof; Pawel Urzyczyn (CSL, 2012)

Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis. - Boris Düdder; Oliver Garbe; Moritz Martens; Jakob Rehof; Pawel Urzyczyn (ITRS, 2012)

Restricted Positive Quantification Is Not Elementary. - Aleksy Schubert; Pawel Urzyczyn; Daria Walukiewicz-Chrzaszcz (TYPES, 2014)

On the Mints Hierarchy in First-Order Intuitionistic Logic. - Aleksy Schubert; Pawel Urzyczyn; Konrad Zdanowski (Log. Methods Comput. Sci., 2016)

Intuitionistic Games: Determinacy, Completeness, and Normalization. - Pawel Urzyczyn (Stud Logica, 2016)

How Hard Is Positive Quantification? - Aleksy Schubert; Pawel Urzyczyn; Daria Walukiewicz-Chrzaszcz (ACM Trans. Comput. Log., 2016)

First-order Answer Set Programming as Constructive Proof Search. - Aleksy Schubert; Pawel Urzyczyn (Theory Pract. Log. Program., 2018)

Duality in Intuitionistic Propositional Logic. - Pawel Urzyczyn (TYPES, 2020)

Kripke Semantics for Intersection Formulas. - Andrej Dudenhefner; Pawel Urzyczyn (ACM Trans. Comput. Log., 2021)

Between proof construction and SAT-solving. - Aleksy Schubert; Pawel Urzyczyn; Konrad Zdanowski (CoRR, 2024)

The existential fragment of second-order propositional intuitionistic logic is undecidable. - Ken-etsu Fujita; Aleksy Schubert; Pawel Urzyczyn; Konrad Zdanowski (J. Appl. Non Class. Logics, 2024)