Pawel Urzyczyn

ACM Trans. Comput. Log., 2021

2020

Duality in Intuitionistic Propositional Logic.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

2018

First-order Answer Set Programming as Constructive Proof Search.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2018

2016

How Hard Is Positive Quantification?

[BibT_eX]

[DOI]

Daria Walukiewicz-Chrzaszcz

ACM Trans. Comput. Log., 2016

Intuitionistic Games: Determinacy, Completeness, and Normalization.

[BibT_eX]

[DOI]

Stud Logica, 2016

On the Mints Hierarchy in First-Order Intuitionistic Logic.

[BibT_eX]

[DOI]

Konrad Zdanowski

Log. Methods Comput. Sci., 2016

2014

Restricted Positive Quantification Is Not Elementary.

[BibT_eX]

[DOI]

Daria Walukiewicz-Chrzaszcz

Proceedings of the 20th International Conference on Types for Proofs and Programs, 2014

2012

Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Sixth Workshop on Intersection Types and Related Systems, 2012

Bounded Combinatory Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic (CSL'12), 2012

The Complexity of Inhabitation with Explicit Intersection.

[BibT_eX]

[DOI]

Jakob Rehof

Proceedings of the Logic and Program Semantics, 2012

2011

Finite Combinatory Logic with Intersection Types.

[BibT_eX]

[DOI]

Jakob Rehof

Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

2010

A Syntactic Embedding of Predicate Logic into Second-Order Propositional Logic.

[BibT_eX]

[DOI]

Morten Heine Sørensen

Notre Dame J. Formal Log., 2010

The Logic of Persistent Intersection.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2010

Preface.

[BibT_eX]

[DOI]

Anna Gambin

Damian Niwinski

Fundam. Informaticae, 2010

2009

Inhabitation of Low-Rank Intersection Types.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

2008

Strong cut-elimination in sequent calculus using Klop's iota-translation and perpetual reductions.

[BibT_eX]

[DOI]

Morten Heine Sørensen

J. Symb. Log., 2008

2007

In the Search of a Naive Type Theory.

[BibT_eX]

[DOI]

Agnieszka Kozubek

Proceedings of the Types for Proofs and Programs, International Conference, 2007

2005

Typed Lambda Calculi and Applications 2003, Selected Papers.

[BibT_eX]

[DOI]

Martin Hofmann

Fundam. Informaticae, 2005

Unsafe Grammars and Panic Automata.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

2004

My (Un)Favourite Things.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

A Simple Proof of the Undecidability of Strong Normalisation.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2003

Type Inference for Nested Self Types.

[BibT_eX]

[DOI]

Viviana Bono

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

2002

The Subtyping Problem for Second-Order Types Is Undecidable.

[BibT_eX]

[DOI]

Inf. Comput., 2002

Retractions of Types with Many Atoms

[BibT_eX]

[DOI]

Laurent Regnier

CoRR, 2002

Higher-Order Pushdown Trees Are Easy.

[BibT_eX]

[DOI]

Teodor Knapik

Damian Niwinski

Proceedings of the Foundations of Software Science and Computation Structures, 2002

2001

Deciding Monadic Theories of Hyperalgebraic Trees.

[BibT_eX]

[DOI]

Teodor Knapik

Damian Niwinski

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

1999

The Emptiness Problem for Intersection Types.

[BibT_eX]

[DOI]

J. Symb. Log., 1999

Alpha-Conversion and Typability.

[BibT_eX]

[DOI]

Simona Ronchi Della Rocca

Mariangiola Dezani-Ciancaglini

Inf. Comput., 1999

Discrimination by Parallel Observers: The Algorithm.

[BibT_eX]

[DOI]

Inf. Comput., 1999

Type Fixpoints: Iteration vs. Recursion.

[BibT_eX]

[DOI]

Zdzislaw Splawski

Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

1997

Type Reconstruction in F<sub>omega</sub>.

[BibT_eX]

[DOI]

Simona Ronchi Della Rocca

Math. Struct. Comput. Sci., 1997

Comparing Cubes of Typed and Type Assignment Systems.

[BibT_eX]

[DOI]

Steffen van Bakel

Luigi Liquori

Ann. Pure Appl. Log., 1997

Inhabitation in Typed Lambda-Calculi (A Syntactic Approach).

[BibT_eX]

[DOI]

Mariangiola Dezani-Ciancaglini

Proceedings of the Typed Lambda Calculi and Applications, 1997

Discrimination by Parallel Observers.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

1996

Positive Recursive Type Assignment.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1996

1994

An Analysis of ML Typability.

[BibT_eX]

[DOI]

Simona Ronchi Della Rocca

J. ACM, 1994

Comparing Cubes.

[BibT_eX]

[DOI]

Steffen van Bakel

Luigi Liquori

Proceedings of the Logical Foundations of Computer Science, Third International Symposium, 1994

1993

The Undecidability of the Semi-unification Problem

[BibT_eX]

[DOI]

Inf. Comput., January, 1993

Type Reconstruction in the Presence of Polymorphic Recursion.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 1993

Primitive Recursion with Extential Types.

[BibT_eX]

Fundam. Informaticae, 1993

Type reconstruction in F-omega is undecidable.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1993

1992

On the Expressive Power of Finitely and Universally Polymorphic Recursive Procedures.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1992

1990

The Undecidability of the Semi-Unification Problem (Preliminary Report)

[BibT_eX]

[DOI]

Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, 1990

ML Typability is DEXTIME-Complete.

[BibT_eX]

[DOI]

Proceedings of the CAAP '90, 1990

1989

Computational Consequences and Partial Solutions of a Generalized Unification Problem (Partial Report)

[BibT_eX]

[DOI]

Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

Algo-Like Languages with Higher-Order Procedures and Their Expressive Power.

[BibT_eX]

[DOI]

Proceedings of the Logic at Botik '89, 1989

1988

Some Relationships Between Logics of Programs and Complexity Theory.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1988

A Proper Extension of ML with an Effective Type-Assignment.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, 1988

On the Computational Power of Universally Polymorphic Recursion

[BibT_eX]

[DOI]

Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

1987

The Hierarchy of Finitely Typed Functional Programs (Short Version)

[BibT_eX]

Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

Verification of Programs with Higher-Order Arrays.

[BibT_eX]

[DOI]

Wojciech Kowalczyk

Proceedings of the Fundamentals of Computation Theory, 1987

1986

"During" Cannot be Expressed by "After".

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1986

1985

Necessary and Sufficient Conditions for the Universality of Programming Formalisms.

[BibT_eX]

[DOI]

Acta Informatica, 1985

1984

Remarks on Comparing Expressive Power of Logics of Programs.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 1984, 1984

1983

A Necessary and Sufficient Condition in Order That a Herbrand Interpretation Be Expressive Relative to Recursive Programs

[BibT_eX]

[DOI]

Inf. Control., March, 1983

Nontrivial Definability by Flow-Chart Programs

[BibT_eX]

[DOI]

Inf. Control., 1983

Necessary and Sufficient Conditions for University of Programming Formalisms (Partial Report).

[BibT_eX]

[DOI]

Proceedings of the Logics of Programs, 1983

Some Relationships between Logics of Programs and Complexity Theory (Extended Abstract)

[BibT_eX]

[DOI]

Proceedings of the 24th Annual Symposium on Foundations of Computer Science, 1983

Deterministic Context-Free Dynamic Logic is More Expressive than Deterministic Dynamic Logic of Regular Programs.

[BibT_eX]

[DOI]

Proceedings of the Fundamentals of Computation Theory, 1983

1981

The Unwind Property in Certain Algebras

[BibT_eX]

[DOI]

Inf. Control., August, 1981

Algorithmic triviality of abstract structures.

[BibT_eX]