VLDB 2026 Research / reviewers in the wild / expert
Jerzy Tiuryn
dblp:t/JerzyTiuryn
· DBLP profile ↗
75ranked-venue papers
29as first author
2since 2021 · last 2022
0000-0002-0285-5606ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 54 · 28 first-author · 1 since 2021Applied, interdisciplinary, general and emerging computing · 18 · 1 first-author · 1 since 2021Software engineering, systems software and programming languages · 2Databases, data management, data science and information retrieval · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2022 | Rooting Gene Trees via Phylogenetic NetworksabstractAbstract Gene trees inferred from alignments of molecular sequences are usually unrooted. Since the root of a gene tree is often the desired property, one of the most classical problems in computational biology is gene tree rooting, where the goal is to infer the most credible rooting edge in an unrooted gene tree. One way to solve it is to apply unrooted reconciliation, where the rooting edge is postulated based on a given split of a rooted species tree. Here, we address a novel variant of the rooting problem, where the gene tree root is inferred using a given phylogenetic network of the species present in the gene tree. One can apply unrooted reconciliation to obtain the best rooting, where the unrooted gene tree is jointly reconciled with a set of splits inferred from the given network. Natural candidates are splits induced by display trees of the network. However, such an approach is computationally prohibiting due to the exponential size of the set. Therefore, we propose a broader and easier-to-control set of splits based on the structural properties of the network. Next, we derive exact mathematical formulas for the rooting problem with the algorithm that runs in square time and space. We verify the algorithm’s quality based on simulated gene trees and networks. Jerzy Tiuryn, Natalia Rutecka, Pawel Górecki 0001 |
COCOON | 1 |
| 2021 | The Unconstrained Diameters of the Duplication-Loss Cost and the Loss CostabstractTree reconciliation costs are a popular choice to account for the discordance between the evolutionary history of a gene family (i.e., a gene tree), and the species tree through which this family has evolved. This discordance is accounted for by the minimum number of postulated evolutionary events necessary for reconciling the two trees. Such events include gene duplication, loss, and deep coalescence, and are used to define different types of tree reconciliation costs. For example, the duplication-loss cost for a gene tree and species tree accounts for the minimum number of gene duplications and losses necessary to reconcile these trees. Fundamental to the understanding of how gene trees and species trees relate to each other are the diameters of tree reconciliation costs. While such diameters have been well-researched, still absent from these studies are the unconstrained diameters for two of the classic tree reconciliation costs, namely the duplication-loss cost and the loss cost. Here, we show the essential mathematical properties of these diameters and provide efficient solutions for computing them. Finally, we analyze the distributions of these diameters using simulated datasets. Pawel Górecki 0001, Oliver Eulenstein, Jerzy Tiuryn |
IEEE ACM Trans. Comput. Biol. Bioinform. | 3 |
| 2019 | Learning signaling networks from combinatorial perturbations by exploiting siRNA off-target effectsabstractMOTIVATION: Perturbation experiments constitute the central means to study cellular networks. Several confounding factors complicate computational modeling of signaling networks from this data. First, the technique of RNA interference (RNAi), designed and commonly used to knock-down specific genes, suffers from off-target effects. As a result, each experiment is a combinatorial perturbation of multiple genes. Second, the perturbations propagate along unknown connections in the signaling network. Once the signal is blocked by perturbation, proteins downstream of the targeted proteins also become inactivated. Finally, all perturbed network members, either directly targeted by the experiment, or by propagation in the network, contribute to the observed effect, either in a positive or negative manner. One of the key questions of computational inference of signaling networks from such data are, how many and what combinations of perturbations are required to uniquely and accurately infer the model? RESULTS: Here, we introduce an enhanced version of linear effects models (LEMs), which extends the original by accounting for both negative and positive contributions of the perturbed network proteins to the observed phenotype. We prove that the enhanced LEMs are identified from data measured under perturbations of all single, pairs and triplets of network proteins. For small networks of up to five nodes, only perturbations of single and pairs of proteins are required for identifiability. Extensive simulations demonstrate that enhanced LEMs achieve excellent accuracy of parameter estimation and network structure learning, outperforming the previous version on realistic data. LEMs applied to Bartonella henselae infection RNAi screening data identified known interactions between eight nodes of the infection network, confirming high specificity of our model and suggested one new interaction. AVAILABILITY AND IMPLEMENTATION: https://github.com/EwaSzczurek/LEM. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online. Jerzy Tiuryn, Ewa Szczurek |
Bioinform. | 1 |
| 2016 | Romulus: robust multi-state identification of transcription factor binding sites from DNase-seq dataabstractMOTIVATION: Computational prediction of transcription factor (TF) binding sites in the genome remains a challenging task. Here, we present Romulus, a novel computational method for identifying individual TF binding sites from genome sequence information and cell-type-specific experimental data, such as DNase-seq. It combines the strengths of previous approaches, and improves robustness by reducing the number of free parameters in the model by an order of magnitude. RESULTS: We show that Romulus significantly outperforms existing methods across three sources of DNase-seq data, by assessing the performance of these tools against ChIP-seq profiles. The difference was particularly significant when applied to binding site prediction for low-information-content motifs. Our method is capable of inferring multiple binding modes for a single TF, which differ in their DNase I cut profile. Finally, using the model learned by Romulus and ChIP-seq data, we introduce Binding in Closed Chromatin (BCC) as a quantitative measure of TF pioneer factor activity. Uniquely, our measure quantifies a defining feature of pioneer factors, namely their ability to bind closed chromatin. AVAILABILITY AND IMPLEMENTATION: Romulus is freely available as an R package at http://github.com/ajank/Romulus CONTACT: [email protected] SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online. Aleksander Jankowski, Jerzy Tiuryn, Shyam Prabhakar |
Bioinform. | 2 |
| 2014 | eCAMBer: efficient support for large-scale comparative analysis of multiple bacterial strainsabstractBACKGROUND: Inconsistencies are often observed in the genome annotations of bacterial strains. Moreover, these inconsistencies are often not reflected by sequence discrepancies, but are caused by wrongly annotated gene starts as well as mis-identified gene presence. Thus, tools are needed for improving annotation consistency and accuracy among sets of bacterial strain genomes. RESULTS: We have developed eCAMBer, a tool for efficiently supporting comparative analysis of multiple bacterial strains within the same species. eCAMBer is a highly optimized revision of our earlier tool, CAMBer, scaling it up for significantly larger datasets comprising hundreds of bacterial strains. eCAMBer works in two phases. First, it transfers gene annotations among all considered bacterial strains. In this phase, it also identifies homologous gene families and annotation inconsistencies. Second, eCAMBer, tries to improve the quality of annotations by resolving the gene start inconsistencies and filtering out gene families arising from annotation errors propagated in the previous phase. CONCLUSIONS: [corrected] eCAMBer efficiently identifies and resolves annotation inconsistencies among closely related bacterial genomes. It outperforms other competing tools both in terms of running time and accuracy of produced annotations. Software, user manual, and case study results are available at the project website: http://bioputer.mimuw.edu.pl/ecamber. Michal Wozniak 0002, Limsoon Wong, Jerzy Tiuryn |
BMC Bioinform. | 3 |
| 2013 | Bioinformatics and Computational Biology in PolandabstractThe series of articles in PLOS Computational Biology on the development of bioinformatics activities in various countries, e.g., China [1], Australia [2], and Singapore [3], and the formation and successful development of the Polish Bioinformatics Society over the last five years, have inspired us to present a personal perspective on the advances of bioinformatics in Poland. Janusz M. Bujnicki, Jerzy Tiuryn |
PLoS Comput. Biol. | 2 |
| 2013 | Unrooted Tree Reconciliation: A Unified ApproachabstractTree comparison functions are widely used in phylogenetics for comparing evolutionary trees. Unrooted trees can be compared with rooted trees by identifying all rootings of the unrooted tree that minimize some provided comparison function between two rooted trees. The plateau property is satisfied by the provided function, if all optimal rootings form a subtree, or plateau, in the unrooted tree, from which the rootings along every path toward a leaf have monotonically increasing costs. This property is sufficient for the linear-time identification of all optimal rootings and rooting costs. However, the plateau property has only been proven for a few rooted comparison functions, requiring individual proofs for each function without benefitting from inherent structural features of such functions. Here, we introduce the consistency condition that is sufficient for a general function to satisfy the plateau property. For consistent functions, we introduce general linear-time solutions that identify optimal rootings and all rooting costs. Further, we identify novel relationships between consistent functions in terms of plateaus, especially the plateau of the well-studied duplication-loss function is part of a plateau of every other consistent function. We introduce a novel approach for identifying consistent cost functions by defining a formal language of Boolean costs. Formulas in this language can be interpreted as cost functions. Finally, we demonstrate the performance of our general linear-time solutions in practice using empirical and simulation studies. Pawel Górecki 0001, Oliver Eulenstein, Jerzy Tiuryn |
IEEE ACM Trans. Comput. Biol. Bioinform. | 3 |
| 2011 | CAMBerVis: visualization software to support comparative analysis of multiple bacterial strainsabstractMOTIVATION: A number of inconsistencies in genome annotations are documented among bacterial strains. Visualization of the differences may help biologists to make correct decisions in spurious cases. RESULTS: We have developed a visualization tool, CAMBerVis, to support comparative analysis of multiple bacterial strains. The software manages simultaneous visualization of multiple bacterial genomes, enabling visual analysis focused on genome structure annotations. AVAILABILITY: The CAMBerVis software is freely available at the project website: http://bioputer.mimuw.edu.pl/camber. Input datasets for Mycobacterium tuberculosis and Staphylocacus aureus are integrated with the software as examples. CONTACT: [email protected] SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online. Michal Wozniak 0002, Limsoon Wong, Jerzy Tiuryn |
Bioinform. | 3 |
| 2011 | Deregulation upon DNA damage revealed by joint analysis of context-specific perturbation dataabstractBACKGROUND: Deregulation between two different cell populations manifests itself in changing gene expression patterns and changing regulatory interactions. Accumulating knowledge about biological networks creates an opportunity to study these changes in their cellular context. RESULTS: We analyze re-wiring of regulatory networks based on cell population-specific perturbation data and knowledge about signaling pathways and their target genes. We quantify deregulation by merging regulatory signal from the two cell populations into one score. This joint approach, called JODA, proves advantageous over separate analysis of the cell populations and analysis without incorporation of knowledge. JODA is implemented and freely available in a Bioconductor package 'joda'. CONCLUSIONS: Using JODA, we show wide-spread re-wiring of gene regulatory networks upon neocarzinostatin-induced DNA damage in Human cells. We recover 645 deregulated genes in thirteen functional clusters performing the rich program of response to damage. We find that the clusters contain many previously characterized neocarzinostatin target genes. We investigate connectivity between those genes, explaining their cooperation in performing the common functions. We review genes with the most extreme deregulation scores, reporting their involvement in response to DNA damage. Finally, we investigate the indirect impact of the ATM pathway on the deregulated genes, and build a hypothetical hierarchy of direct regulation. These results prove that JODA is a step forward to a systems level, mechanistic understanding of changes in gene regulation between different cell populations. Ewa Szczurek, Florian Markowetz, Irit Gat-Viks, Przemyslaw Biecek, Jerzy Tiuryn, Martin Vingron |
BMC Bioinform. | 5 |
| 2010 | CAMBer: An approach to support comparative analysis of multiple bacterial strainsabstractThere is a large amount of inconsistency in gene structure annotations of bacterial strains. This inconsistency is a frustrating impedance to effective comparative genomic analysis of bacterial strains in promising applications such as gaining insights into bacterial drug resistance. Here, we propose CAMBer as an approach to support comparative analysis of multiple bacterial strains. CAMBer produces what we called multigene families. Each multigene family reveals genes that are in one-to-one correspondence in the bacterial strains, thereby permitting their annotations to be integrated. As a result, more accurate and more comprehensive annotations of the bacterial strains can be produced. Michal Wozniak 0002, Limsoon Wong, Jerzy Tiuryn |
BIBM | 3 |
| 2010 | MODEVO: exploring modularity and evolution of protein interaction networksabstractSUMMARY: Interrogating protein complexes and pathways in an evolutionary context provides insights into the formation of the basic functional components of the cell. We developed two independent Cytoscape plugins that can be cooperatively used to map evolving protein interaction networks at the module level. The APCluster plugin implements a recent affinity propagation (AP) algorithm for graph clustering and can be applied to decompose networks into coherent modules. The NetworkEvolution plugin provides the capability to visualize selected modules in consecutive evolutionary stages. AVAILABILITY: The plugins, input data and usage scenarios are freely available from the project web site: http://bioputer.mimuw.edu.pl/modevo. The plugins are also available from the Cytoscape plugin repository. Michal Wozniak 0002, Jerzy Tiuryn, Janusz Dutkowski |
Bioinform. | 2 |
| 2009 | Phylogeny-guided interaction mapping in seven eukaryotesabstractBACKGROUND: The assembly of reliable and complete protein-protein interaction (PPI) maps remains one of the significant challenges in systems biology. Computational methods which integrate and prioritize interaction data can greatly aid in approaching this goal. RESULTS: We developed a Bayesian inference framework which uses phylogenetic relationships to guide the integration of PPI evidence across multiple datasets and species, providing more accurate predictions. We apply our framework to reconcile seven eukaryotic interactomes: H. sapiens, M. musculus, R. norvegicus, D. melanogaster, C. elegans, S. cerevisiae and A. thaliana. Comprehensive GO-based quality assessment indicates a 5% to 44% score increase in predicted interactomes compared to the input data. Further support is provided by gold-standard MIPS, CYC2008 and HPRD datasets. We demonstrate the ability to recover known PPIs in well-characterized yeast and human complexes (26S proteasome, endosome and exosome) and suggest possible new partners interacting with the putative SWI/SNF chromatin remodeling complex in A. thaliana. CONCLUSION: Our phylogeny-guided approach compares favorably to two standard methods for mapping PPIs across species. Detailed analysis of predictions in selected functional modules uncovers specific PPI profiles among homologous proteins, establishing interaction-based partitioning of protein families. Provided evidence also suggests that interactions within core complex subunits are in general more conserved and easier to transfer accurately to other organisms, than interactions between these subunits. Janusz Dutkowski, Jerzy Tiuryn |
BMC Bioinform. | 2 |
| 2009 | Finding evolutionarily conserved cis-regulatory modules with a universal set of motifsabstractBACKGROUND: Finding functional regulatory elements in DNA sequences is a very important problem in computational biology and providing a reliable algorithm for this task would be a major step towards understanding regulatory mechanisms on genome-wide scale. Major obstacles in this respect are that the fact that the amount of non-coding DNA is vast, and that the methods for predicting functional transcription factor binding sites tend to produce results with a high percentage of false positives. This makes the problem of finding regions significantly enriched in binding sites difficult. RESULTS: We develop a novel method for predicting regulatory regions in DNA sequences, which is designed to exploit the evolutionary conservation of regulatory elements between species without assuming that the order of motifs is preserved across species. We have implemented our method and tested its predictive abilities on various datasets from different organisms. CONCLUSION: We show that our approach enables us to find a majority of the known CRMs using only sequence information from different species together with currently publicly available motif data. Also, our method is robust enough to perform well in predicting CRMs, despite differences in tissue specificity and even across species, provided that the evolutionary distances between compared species do not change substantially. The complexity of the proposed algorithm is polynomial, and the observed running times show that it may be readily applied. Bartek Wilczynski, Norbert Dojer, Mateusz Patelak, Jerzy Tiuryn |
BMC Bioinform. | 4 |
| 2007 | Inferring phylogeny from whole genomesabstractMOTIVATION: Inferring species phylogenies with a history of gene losses and duplications is a challenging and an important task in computational biology. This problem can be solved by duplication-loss models in which the primary step is to reconcile a rooted gene tree with a rooted species tree. Most modern methods of phylogenetic reconstruction (from sequences) produce unrooted gene trees. This limitation leads to the problem of transforming unrooted gene tree into a rooted tree, and then reconciling rooted trees. The main questions are 'What about biological interpretation of choosing rooting?', 'Can we find efficiently the optimal rootings?', 'Is the optimal rooting unique?'. RESULTS: In this paper we present a model of reconciling unrooted gene tree with a rooted species tree, which is based on a concept of choosing rooting which has minimal reconciliation cost. Our analysis leads to the surprising property that all the minimal rootings have identical distributions of gene duplications and gene losses in the species tree. It implies, in our opinion, that the concept of an optimal rooting is very robust, and thus biologically meaningful. Also, it has nice computational properties. We present a linear time and space algorithm for computing optimal rooting(s). This algorithm was used in two different ways to reconstruct the optimal species phylogeny of five known yeast genomes from approximately 4700 gene trees. Moreover, we determined locations (history) of all gene duplications and gene losses in the final species tree. It is interesting to notice that the top five species trees are the same for both methods. AVAILABILITY: Software and documentation are freely available from http://bioputer.mimuw.edu.pl/~gorecki/urec Pawel Górecki 0001, Jerzy Tiuryn |
Bioinform. | 2 |
| 2007 | URec: a system for unrooted reconciliationabstractUNLABELLED: URec is a software based on a concept of unrooted reconciliation. It can be used to reconcile a set of unrooted gene trees with a rooted species tree or a set of rooted species trees. Moreover, it computes detailed distribution of gene duplications and gene losses in a species tree. It can be used to infer optimal species phylogenies for a given set of gene trees. URec is implemented in C++ and can be easily compiled under Unix and Windows systems. AVAILABILITY: Software is freely available for download from our website at http://bioputer.mimuw.edu.pl/~gorecki/urec. This webpage also contains Windows executables and a number of advanced examples with explanations. Pawel Górecki 0001, Jerzy Tiuryn |
Bioinform. | 2 |
| 2007 | A new approach to the assessment of the quality of predictions of transcription factor binding sites
Szymon Nowakowski, Jerzy Tiuryn |
J. Biomed. Informatics | 2 |
| 2006 | On Genome Evolution with Innovation
Damian Wójtowicz, Jerzy Tiuryn |
MFCS | 2 |
| 2006 | Applying dynamic Bayesian networks to perturbed gene expression dataabstractBACKGROUND: A central goal of molecular biology is to understand the regulatory mechanisms of gene transcription and protein synthesis. Because of their solid basis in statistics, allowing to deal with the stochastic aspects of gene expressions and noisy measurements in a natural way, Bayesian networks appear attractive in the field of inferring gene interactions structure from microarray experiments data. However, the basic formalism has some disadvantages, e.g. it is sometimes hard to distinguish between the origin and the target of an interaction. Two kinds of microarray experiments yield data particularly rich in information regarding the direction of interactions: time series and perturbation experiments. In order to correctly handle them, the basic formalism must be modified. For example, dynamic Bayesian networks (DBN) apply to time series microarray data. To our knowledge the DBN technique has not been applied in the context of perturbation experiments. RESULTS: We extend the framework of dynamic Bayesian networks in order to incorporate perturbations. Moreover, an exact algorithm for inferring an optimal network is proposed and a discretization method specialized for time series data from perturbation experiments is introduced. We apply our procedure to realistic simulations data. The results are compared with those obtained by standard DBN learning techniques. Moreover, the advantages of using exact learning algorithm instead of heuristic methods are analyzed. CONCLUSION: We show that the quality of inferred networks dramatically improves when using data from perturbation experiments. We also conclude that the exact algorithm should be used when it is possible, i.e. when considered set of genes is small enough. Norbert Dojer, Anna Gambin, Andrzej Mizera, Bartek Wilczynski, Jerzy Tiuryn |
BMC Bioinform. | 5 |
| 2006 | Using local gene expression similarities to discover regulatory binding site modulesabstractBACKGROUND: We present an approach designed to identify gene regulation patterns using sequence and expression data collected for Saccharomyces cerevisae. Our main goal is to relate the combinations of transcription factor binding sites (also referred to as binding site modules) identified in gene promoters to the expression of these genes. The novel aspects include local expression similarity clustering and an exact IF-THEN rule inference algorithm. We also provide a method of rule generalization to include genes with unknown expression profiles. RESULTS: We have implemented the proposed framework and tested it on publicly available datasets from yeast S. cerevisae. The testing procedure consists of thorough statistical analyses of the groups of genes matching the rules we infer from expression data against known sets of co-regulated genes. For this purpose we have used published ChIP-Chip data and Gene Ontology annotations. In order to make these tests more objective we compare our results with recently published similar studies. CONCLUSION: Results we obtain show that local expression similarity clustering greatly enhances overall quality of the derived rules, both in terms of enrichment of Gene Ontology functional annotation and coherence with ChIP-Chip binding data. Our approach thus provides reliable hypotheses on co-regulation that can be experimentally verified. An important feature of the method is its reliance only on widely accessible sequence and expression data. The same procedure can be easily applied to other microbial organisms. Bartek Wilczynski, Torgeir R. Hvidsten, Andriy Kryshtafovych, Jerzy Tiuryn, Jan Komorowski, Krzysztof Fidelis |
BMC Bioinform. | 4 |
| 2006 | DLS-trees: A model of evolutionary scenarios
Pawel Górecki 0001, Jerzy Tiuryn |
Theor. Comput. Sci. | 2 |
| 2004 | A Case Study of Genome Evolution: From Continuous to Discrete Time Model
Jerzy Tiuryn, Ryszard Rudnicki, Damian Wójtowicz |
MFCS | 1 |
| 2003 | Substructural logic and partial correctnessabstractWe formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and trace models. As a corollary, we obtain a complete sequent calculus for inclusion and equivalence of regular expressions. Dexter Kozen, Jerzy Tiuryn |
ACM Trans. Comput. Log. | 2 |
| 2002 | Products and Polymorphic Subtypes
Viviana Bono, Jerzy Tiuryn |
Fundam. Informaticae | 2 |
| 2002 | The Subtyping Problem for Second-Order Types Is Undecidable
Jerzy Tiuryn, Pawel Urzyczyn |
Inf. Comput. | 1 |
| 2001 | Intuitionistic Linear Logic and Partial CorrectnessabstractWe formulate a Gentzen-style sequent calculus for partial correctness that subsumes propositional Hoare logic. The system is a noncommutative intuitionistic linear logic. We prove soundness and completeness over relational and trace models. As a corollary, we obtain a complete sequent calculus for the inclusion and equivalence of regular expressions. Dexter Kozen, Jerzy Tiuryn |
LICS | 2 |
| 2001 | A Sequent Calculus for Subtyping Polymorphic Types
Jerzy Tiuryn |
Inf. Comput. | 1 |
| 2001 | On the completeness of propositional Hoare logic
Dexter Kozen, Jerzy Tiuryn |
Inf. Sci. | 2 |
| 1999 | Type Reconstruction for Functional Programs with Subtyping over a Lattice of Atomic Types
Jerzy Tiuryn |
MFCS | 1 |
| 1999 | Discrimination by Parallel Observers: The Algorithm
Mariangiola Dezani-Ciancaglini, Jerzy Tiuryn, Pawel Urzyczyn |
Inf. Comput. | 2 |
| 1999 | Alpha-Conversion and TypabilityabstractThere are two results in this paper. We first prove that alpha-conversion on types can be eliminated from the second-order λ -calculus F of Girard and Reynolds without affecting the typing power of the system. On the other hand we show that it is impossible to eliminate alpha-conversion on universally quantified variables in the higher-order λ -calculus F ω of Girard, by exhibiting a term which is typable in F ω with alpha-conversion but not typable in F ω without alpha-conversion. Assaf J. Kfoury, Simona Ronchi Della Rocca, Jerzy Tiuryn, Pawel Urzyczyn |
Inf. Comput. | 3 |
| 1997 | Discrimination by Parallel ObserversabstractThe main result of the paper is a proof of the following equivalence: two pure lambda terms are observationally equivalent in the lazy concurrent lambda calculus if they have the same Levy-Longo trees. It follows that contextual equivalence coincides with behavioural equivalence (bisimulation) as considered by Sangiorgi (1994). Another consequence is that the discriminating power of concurrent lambda contexts is the same as that of Boudol-Laneve's contexts with multiplicities (1996). Mariangiola Dezani-Ciancaglini, Jerzy Tiuryn, Pawel Urzyczyn |
LICS | 2 |
| 1996 | The Subtyping Problem for Second-Order Types is UndecidableabstractWe prove that the subtyping problem induced by Mitchell's containment relation (1988) for second-order polymorphic types is undecidable. It follows that type-checking is undecidable for the polymorphic lambda-calculus extended by an appropriate subsumption rule. Jerzy Tiuryn, Pawel Urzyczyn |
LICS | 1 |
| 1996 | A Sequent Calculus for Subtyping Polymorphic Types
Jerzy Tiuryn |
MFCS | 1 |
| 1996 | Satisfiability of Inequalities in a PosetabstractWe consider tractable and intractable cases of the satisfiability problem for conjunctions of inequalities between variables and constants in a fixed finite poset. We show that crowns are intractable. We study members and closure properties of the cl Vaughan R. Pratt, Jerzy Tiuryn |
Fundam. Informaticae | 2 |
| 1995 | Equational Axiomatization of Bicoercibility for Polymorphic Types
Jerzy Tiuryn |
FSTTCS | 1 |
| 1994 | An Analysis of ML TypabilityabstractWe carry out an analysis of typability of terms in ML. Our main result is that this problem is DEXPTIME-hard, where by DEXPTIME we mean DTIME(2 n 0(1) ). This, together with the known exponential-time algorithm that solves the problem, yields the DEXPTIME-completeness result. This settles an open problem of P. Kanellakis and J. C. Mitchell. Part of our analysis is an algebraic characterization of ML typability in terms of a restricted form of semi-unification, which we identify as acyclic semi-unification . We prove that ML typability and acyclic semi-unification can be reduced to each other in polynomial time. We believe this result is of independent interest. Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
J. ACM | 2 |
| 1993 | The Undecidability of the Semi-unification Problem
Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
Inf. Comput. | 2 |
| 1993 | Type Reconstruction in the Presence of Polymorphic RecursionabstractWe study the problem of type-checking functional programs in three extensions of ML.One distinguishing feature of these extensions is that they allow recursive definitions to be polymorphically typed.Although the motivation for these extensions comes from pragmatic considera- Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
ACM Trans. Program. Lang. Syst. | 2 |
| 1992 | Subtype InequalitiesabstractThe satisfiability problem for subtype inequalities in simple types is studied. The naive algorithm that solves this problem runs in nondeterministic exponential time for every predefined poset of atomic subtypings the satisfiability problem for subtype inequalities is PSPACE-hard. On the other hand, it is proved that if the poset of atomic subtypings is a disjoint union of lattices, then the satisfiability problem for subtype inequalities is solvable in PTIME. This result covers the important special case of the unification problem that can be obtained when the atomic subtype relation is equality.> Jerzy Tiuryn |
LICS | 1 |
| 1992 | Type Reconstruction in Finite Rank Fragments of the Second-Order lambda-CalculusabstractThe prove that the problem of type reconstruction in the polymorphic λ-calculus of rank 2 is polynomial-time equivalent to the problem of type reconstruction in ML, and is therefore DEXPTIME-complete. We also prove that for every k > 2, the problem of type reconstruction in the polymorphic λ-calculus of rank k, extended with suitably chosen constants with types of rank 1, is undecidable. Assaf J. Kfoury, Jerzy Tiuryn |
Inf. Comput. | 2 |
| 1992 | On the Expressive Power of Finitely and Universally Polymorphic Recursive ProceduresabstractFinitely typed functional programs are naturally classified by their levels. This syntactic classification of functional programs corresponds to a semantical classification: the higher the level of functional programs, the more functions they can compute. We call FL the language of finitely typed functional programs. The halting problem on finite interpretations is elementary recursive for every FL program, i.e. for every FL program P there is an elementary recursive procedure to decide for every finite interpretation I whether P halts on I. The well-known programming language ML is essentially FL, augmented with the polymorphic let-in constructor. We show that ML computes the same class of functions as FL. As a consequence. Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
Theor. Comput. Sci. | 2 |
| 1990 | Type Reconstruction in Finite-Rank Fragments of the Polymorphic lambda-Calculus (Extended Summary)abstractIt is proven that the problem of type reconstruction in the polymorphic lambda -calculus of rank two is polynomial-time equivalent to the problem of type reconstruction in ML, and is therefore DEXPTIME-complete. It is also proven that for every k>2, the problem of type reconstruction in the polymorphic lambda -calculus of rank k, extended with suitably chosen constants with types of rank one, is undecidable.> Assaf J. Kfoury, Jerzy Tiuryn |
LICS | 2 |
| 1990 | Type Inference Problems: A Survey
Jerzy Tiuryn |
MFCS | 1 |
| 1990 | The Undecidability of the Semi-Unification Problem (Preliminary Report)abstractThe Semi-Unification Problem (SUP) is a natural generalization of both first-order unification and matching.The problem arises in various branches of computer science and logic.Although several special cases of SUP are known to be decidable, the problem in general has been open for several years.We show that SUP in general is undecidable, by reducing what we call the "boundedness problem" of Turing machines to SUP.The undecidability of this boundedness problem is established by a technique developed in the mid-1960's to prove related results about Turing machines, Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
STOC | 2 |
| 1990 | Fixed Points in Free Process Algebras, Part II
Jerzy Tiuryn, David B. Benson |
Theor. Comput. Sci. | 1 |
| 1989 | Computational Consequences and Partial Solutions of a Generalized Unification Problem (Partial Report)abstractA generalization of first-order unification, called semiunification, is studied with two goals in mind: (1) type-checking functional programs relative to an improved polymorphic type discipline; and (2) deciding the typability of terms in a restricted form of the polymorphic lambda -calculus.> Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
LICS | 2 |
| 1989 | A Simplified Proof of DDL < DL
Jerzy Tiuryn |
Inf. Comput. | 1 |
| 1989 | Fixed Points in Free Process Algebras, Part I
David B. Benson, Jerzy Tiuryn |
Theor. Comput. Sci. | 2 |
| 1988 | On the Computational Power of Universally Polymorphic RecursionabstractML/sup +/ is an extension of the functional language ML that allows the actual parameters of recursively called functions to have types that are generic instances of the (derived) types of corresponding formal parameters. It is shown that the polymorphism allowed by the original ML can be eliminated without loss of computational power, specifically, it is shown that its computational power (in all interpretations) is the same as that of finitely typed functional programs. It is proved that the polymorphism of ML/sup +/ cannot be eliminated, in that its computational power far exceeds that of finitely typed functional programs and therefore that of the original ML too.> Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
LICS | 2 |
| 1988 | A Proper Extension of ML with an Effective Type-AssignmentabstractWe extend the functional language ML by allowing the recursive calls to a function F on the right-hand side of its definition to be at different types, all generic instances of the (derived) type of F on the left-hand side of its definition. The original definition of ML does not allow this feature. This extension does not produce new types beyond the usual universal polymorphic types of ML and satisfies the properties already enjoyed by ML: the principal-type property and the effective type-assignment property. Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
POPL | 2 |
| 1988 | Some Relationships Between Logics of Programs and Complexity Theory
Jerzy Tiuryn, Pawel Urzyczyn |
Theor. Comput. Sci. | 1 |
| 1987 | The Hierarchy of Finitely Typed Functional Programs (Short Version)
Assaf J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
LICS | 2 |
| 1986 | Higher-Order Arrays and Stacks in Programming. An Application of Complexity Theory to Logics of Programs
Jerzy Tiuryn |
MFCS | 1 |
| 1985 | Preface
Jerzy Tiuryn |
Inf. Control. | 1 |
| 1984 | Remarks on Comparing Expressive Power of Logics of Programs
Jerzy Tiuryn, Pawel Urzyczyn |
MFCS | 1 |
| 1984 | Unbounded Program Memory Adds to the Expressive Power of First-Order Programming Logic
Jerzy Tiuryn |
Inf. Control. | 1 |
| 1984 | Equivalences among Logics of Programs
Albert R. Meyer, Jerzy Tiuryn |
J. Comput. Syst. Sci. | 2 |
| 1983 | Some Relationships between Logics of Programs and Complexity Theory (Extended Abstract)abstractThe aim of this paper is to show that some open problems in Comparative Schematology and in Logics of Programs are equivalent to open problems in Complexity Theory. In particular we show that PSPACE = PTIME holds if and only if flow-diagrams with arrays are of the same computational power as recursive procedures. These statements are also equivalent to the following statement: Logics based on the above-mentioned classes of program schemes have equal expressive power. A similar characterization may be given for other complexity classes. Jerzy Tiuryn, Pawel Urzyczyn |
FOCS | 1 |
| 1982 | On the Power of Nondeterminism in Dynamic Logic
Piotr Berman, Joseph Y. Halpern, Jerzy Tiuryn |
ICALP | 3 |
| 1982 | Another Incompleteness Result for Hoare's Logic
Jan A. Bergstra, Anna Chmielinska, Jerzy Tiuryn |
Inf. Control. | 3 |
| 1982 | Floyds Principle, Correctness Theories and Program Equivalence
Jan A. Bergstra, Jerzy Tiuryn, John V. Tucker |
Theor. Comput. Sci. | 2 |
| 1981 | Unbounded Program Memory Adds to the Expressive Power of First-Order Dynamic Logic (Extended Abstract)abstractThe aim of this paper is to-compare various logics of programs with respect to their expressibility. The main result of the paper states that no logic of bounded memory programs is capable of defining the algebra of standard binary trees T = (T, CONS, NIL). Since the usual logics of unbounded memory programs are able to define the above algebra - we derive from the main result a couple of results which solve some questions about comparing expressive powers of programming logics. Jerzy Tiuryn |
FOCS | 1 |
| 1981 | Logic of effective definitions
Jan A. Bergstra, Jerzy Tiuryn |
Fundam. Informaticae | 2 |
| 1981 | Algorithmic degrees of algebraic structures
Jan A. Bergstra, Jerzy Tiuryn |
Fundam. Informaticae | 2 |
| 1981 | Regular extensions of iterative algebras and metric interpretations
Jan A. Bergstra, Jerzy Tiuryn |
Fundam. Informaticae | 2 |
| 1981 | Logic of effective definitions
Jerzy Tiuryn |
Fundam. Informaticae | 1 |
| 1980 | Unique Fixed Points Vs. Least Fixed Points
Jerzy Tiuryn |
Theor. Comput. Sci. | 1 |
| 1979 | Implicit definability of algebraic structures by means of program properties
Jan A. Bergstra, Jerzy Tiuryn |
FCT | 2 |
| 1979 | Unique Fixed Points v. Least Fixed Points
Jerzy Tiuryn |
ICALP | 1 |
| 1979 | Fixed Points in the Power-Set Algebra of Infinite Trees (Abstract)
Jerzy Tiuryn |
MFCS | 1 |
| 1978 | Some Results on the Decomposition of Finite Automata
Jerzy Tiuryn |
Inf. Control. | 1 |
| 1977 | Fixed-Points and Algebras with Infinitely Long Expressions, II
Jerzy Tiuryn |
FCT | 1 |
| 1977 | Fixed-Points and Algebras with Infinitely Long Expressions, I
Jerzy Tiuryn |
MFCS | 1 |
| 1976 | On the Domain of Iteration in Iterative Algebraic Theories
Jerzy Tiuryn |
MFCS | 1 |
| 1974 | The Algebraic Approach to the Theory of Computing Systems
Jerzy Tiuryn |
MFCS | 1 |