BibTex
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Fichier BibTex généré par GRAPPA
% Lille, 2/09/2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%========================== Variables ==========================
@string{AAECC={Applicable Algebra in Engineering Communication and Computing}}
@string{AAMAS={Autonomous Agents and Multi-Agent Systems}}
@string{AC={Acta Cybernetica}}
@string{ACADEMIC={Academic Press}}
@string{ACM={ACM-Press}}
@string{ACMCS={ACM computing surveys}}
@string{ACMSN={ACM SIGPLAN Notices}}
@string{ACMTDS={ACM Transactions of Database Systems}}
@string{ACo={Acta Comportementalia}}
@string{ADDWES={Addison-Wesley}}
@string{Adossa={Adossa}}
@string{AI={Acta Informatica}}
@string{AImaga={AI magazine}}
@string{AInt={Artificial Intelligence}}
@string{AK={Akademiai Kiado}}
@string{Algorithms={Algorithms}}
@string{AMM={American Mathematical Monthly}}
@string{AOM={Annals of Mathematics}}
@string{APAL={Annals of Pure and Applied Logic}}
@string{BAMS={Bulletin of the American Mathematical Society}}
@string{BEATCS={Bulletin of the European Association of Theoretical Computer Science}}
@string{BehaviorBrainSc={Behavioral and Brain Sciences}}
@string{Belin={Belin}}
@string{BIGPL={Bulletin of the Interest Group on Logic Programming}}
@string{BIOINF={Bioinformatics}}
@string{Blackwell={Blackwell}}
@string{BRICS={Basic Research in Computer Science}}
@string{BullIsrael={Bulletin of the Research Concil of Israel}}
@string{BW={Brace and World}}
@string{CACM={Communications of the ACM}}
@string{Cambridge={Cambridge University Press}}
@string{CBT={Cognition and Brain Theory}}
@string{CG={Cognitive Science}}
@string{ChicagoPress={The University of Chicago Press}}
@string{CIJ={Constraints, an International Journal}}
@string{CLSI={CLSI Publications}}
@string{CNRS={Éditions du CNRS,Paris}}
@string{Cog={Cognition}}
@string{Cog-Brain={Cognition and Brain Theory}}
@string{COLIN={Armand Colin, Paris}}
@string{CompLing={Computational Linguistics}}
@string{COMPSL={Computer Speech and Language}}
@string{CPRSR={Calculateurs parallèles, réseaux et systèmes répartis}}
@string{DAM={Discrete Applied Mathematics}}
@string{DAN-SSR={Doklady Akademii Nauk SSSR}}
@string{DM={Discrete Mathematics}}
@string{DMTCS={Discrete Mathematics and Theoretical Computer Science}}
@string{Dunod={Dunod}}
@string{EATCS ={Bulletin of the EATCS}}
@string{ECA={Extraction des connaissances et apprentissage}}
@string{EJC={European Journal of Combinatorics}}
@string{ELSEVIER={Elsevier}}
@string{ENTCS={Electronical notes in theoretical computer science}}
@string{Eyrolles={Eyrolles}}
@string{FI={Fundamenta Informaticae}}
@string{Flammarion={Flammarion}}
@string{Folli={The European Association for Logic, Language and Information}}
@string{FoLLI={The European Association for Logic, Language and Information}}
@string{FOLLI/LNAI={FOLLI/LNAI}}
@string{Grammars={Grammars}}
@string{Hachette={Hachette}}
@string{HAR={Harvester Press}}
@string{Harvard={Harvard University Press}}
@string{HERMES={Hermès}}
@string{IBM={IBM J. of Res. and Dev.}}
@string{ICOMP={Information and Computation}}
@string{ICON={Icon Books}}
@string{ICONT={Information and Control}}
@string{IEEECSP={{IEEE} Comp. Soc. Press}}
@string{IEEE-NN={IEEE Transactions on Neural Networks}}
@string{IEEE-PAMI={IEEE Transactions on Pattern Analysis and Machine Intelligence}}
@string{IEEE-TEC={IEEE Transactions on Evolutionary Computation}}
@string{IEEE-TKDE={IEEE Trans. on Know. Data Eng.}}
@string{IEEE-TOIT={IEEE Transactions on Information Theory}}
@string{IEEETSMC={IEEE Transactions on Systems, Man and Cybernetics}}
@string{IGI={Idea Group Inc.}}
@string{IJFCS={International Journal on Foundations of Computer Science}}
@string{IJPRAI={International Journal of Pattern Recognition and Artificial Intelligence}}
@string{INEQ={Inequalities}}
@string{INSY={Information Systems}}
@string{Intellectica={Intellectica}}
@string{INTER_ED={InterEditions}}
@string{IPL={Information Processing Letters}}
@string{IPTC={The Impact of Processing Techniques on Communications}}
@string{ISJ={Information Sciences Journal}}
@string{ISY={Information Systems}}
@string{itIT={it- Information Technology}}
@string{ITOR={International Transactions in Operation Research}}
@string{ITP={International Thomson Publishing}}
@string{JACM={Journal of the ACM}}
@string{JAIR={Journal of Artificial Intelligence Research}}
@string{JALCO={Journal of Automata, Languages and
Combinatorics}}
@string{JAR={Journal of Automated Reasoning}}
@string{JCB={Journal of Computational Biology}}
@string{JCSS={Journal of Computer and System Science}}
@string{JDL={Journal of Digital Libraries}}
@string{JFP={Journal of Functional Programming}}
@string{JICSLP={Joint International Conference Symposium on Logic Programming}}
@string{JIP={Journal of Information Processing}}
@string{JLC={Journal of Logic and Computation}}
@string{JLP={Journal of Logic Programming}}
@string{JMLR={Journal of Machine Learning Research}}
@string{JMP={Journal of Mathematical Psychology}}
@string{JoLLI={Journal of Logic, Language and Information}}
@string{JRLC={Journal of Research on Language and Computation}}
@string{JRSSA={Journal of the Royal Statistical Society-A}}
@string{JRSSB={Journal of the Royal Statistical Society-B}}
@string{JRSSC={Journal of the Royal Statistical Society-C}}
@string{JRSSD={Journal of the Royal Statistical Society-D}}
@string{JSC={Journal of Symbolic Computation}}
@string{JSL={Journal of Symbolic Logic}}
@string{JSPT={Journal of Simulation Practice and Theory}}
@string{KAP={Kluwer Academic Publishers}}
@string{KAUFM={Morgan Kaufmann}}
@string{KIME={Kimé,Paris}}
@string{Kl={Kluwer}}
@string{LaDecouverte={La Découverte}}
@string{LandP={Linguistics and Philosophy}}
@string{Languages={Languages}}
@string{LawrenceErlbaum={Lawrence Erlbaum}}
@string{LMCS={Logical Methods in Computer Science}}
@string{LNAI={Lecture Notes in Artificial Intelligence}}
@string{LNCS={Lecture Notes in Computer Science}}
@string{Masson={Masson}}
@string{MFCS={Mathematical Foundations of Computer Science}}
@string{MGH={McGraw-Hill}}
@string{Minuit={Minuit}}
@string{MIT={MIT Press}}
@string{MITE={The MIT Encyclopedia of Cognitive Sciences}}
@string{MITP={MIT Press}}
@string{MJBA={Mexican journal of behavior analysis}}
@string{ML={Machine Learning}}
@string{MRI={MRI Symposia Series}}
@string{MSCS={Mathematical Structures in Computer Science}}
@string{MST={Mathematical System Theory}}
@string{NAMS={Notices Amer. Math. Soc.}}
@string{Nature={Nature}}
@string{NC={Neural Computation}}
@string{NH={North-Holland}}
@string{NJC={Nordic Journal of Computing}}
@string{OdileJacob={Odile Jacob}}
@string{oreilly={O'Reilly Media, Inc.}}
@string{OUP={Oxford University Press}}
@string{Payot={Payot}}
@string{PCV={Psychology of Computer Vision}}
@string{PH={Publisher Habile}}
@string{P-IEEE={Proceedings of The IEEE}}
@string{PP={Penguin Press}}
@string{PPNY={Polytechnic Press, Polytechnic Institute of Brooklyn, N.Y.}}
@string{PRENTICE={Prentice-Hall}}
@string{PressPocket={Press Pocket}}
@string{PRL={Pattern Recognition Letters}}
@string{PTAMI={IEEE Transactions on Pattern Analysis and Machine Intelligence}}
@string{PTRS={Philosophical Transactions of the Royal Society}}
@string{PUF={Presses Universitaires de France}}
@string{PUG={Presses Universitaires de Grenoble}}
@string{PUL={PUL, Lille}}
@string{PUP={Princetown University Press}}
@string{RAIRO={RAIRO}}
@string{Reidel={Reidel}}
@string{RIA={Revue d'Intelligence Artificielle}}
@string{RIUR={Readings in Uncertain Reasoning}}
@string{RLV={Recherches Linguistiques de Vincennes}}
@string{SAMS={Systems Analysis Modeling and Simulation}}
@string{SAS={Symposium on Static Analysis}}
@string{SciAm={Scientific American}}
@string{Seuil={Le Seuil}}
@string{SIAMJC={SIAM Journal on Computing}}
@string{SIG={SIGMOD Rec.}}
@string{SIGIRF={SIGIR FORUM}}
@string{SL={Studia Logica}}
@string{SUBICALP={Submitted to ICALP}}
@string{SUP={Stanford University Press}}
@string{SV={Springer Verlag}}
@string{TAL={TAL}}
@string{TAMICS={Text and Monographs in Computer Science}}
@string{TAMS={Transactions of the American Mathematical Society}}
@string{TCS={Theoretical Computer Science}}
@string{TCSB={Transactions on Computational Systems Biology}}
@string{TE={Terminal}}
@string{TIA={Theoretical Informatics and Applications}}
@string{TIT={IEEE Transactions on Information Theory}}
@string{TOCL={ACM Transactions on Computational Logics}}
@string{TODS={ACM Transactions on Database Systems}}
@string{TOIT={ACM Transactions on Internet Technology}}
@string{TOPLAS={ACM Transactions on Programming Languages and Systems}}
@string{TS={Teubner Studienbucher}}
@string{VLDB={VLPB Journal}}
@string{VLDB-2={The VLDB Journal}}
@string{WHF={W.H. Freeman and Co, San Francisco}}
@string{WILEY={John Wiley}}
@string{WS={World Scientific}}
@string{YUP={Yale University Press}}
%========================== Article ==========================
@Article{AlthausDuchierKollerMehlhornNiehrenThiel03,
year = {2003},
title = {An Efficient Graph Algorithm for Dominance Constraints},
journal = Algorithms,
audience = \{Art1},
author = {Ernst Althaus and Denys Duchier and Alexander Koller and Kurt Mehlhorn and Joachim Niehren and Sven Thiel},
month = may,
note = {Special Issue of SODA 2001.},
url = {http://www.ps.uni-sb.de/Papers/paper_info.php?label=eff-dom},
abstract = {Dominance constraints are logical descriptions of trees that are widely used in computational linguistics. Their
general satisfiability problem is known to be NP-complete.
Here we identify normal dominance constraints
and present an efficient graph algorithm for testing their
satisfiablity in deterministic polynomial time. Previously,
no polynomial time algorithm was known.},
auteur = {MOSTRARE STC GRAPPA},
key = {a11},
volume = {48},
number = {1},
pages = {194--219},
}
@Article{CarmeGilleronLemayNiehren07,
title = {Interactive Learning of Node Selecting Tree Transducers},
journal = ML,
audience = \{Art1},
year = "2007",
author = {Julien Carme and Rémi Gilleron and Aurélien Lemay and Joachim Niehren},
abstract = {
We develop new algorithms for learning monadic node selection
queries in unranked trees from annotated examples,
and apply them to visually interactive Web
information extraction.
We propose to represent monadic queries by bottom-up deterministic
Node Selecting Tree Transducers (NSTTs), a particular class of tree
automata that we introduce. We prove that deterministic NSTTs capture
the class of queries definable in monadic second order logic (MSO) in
trees, which Gottlob and Koch (2002) argue to have the right expressiveness for Web
information extraction, and prove that monadic queries defined by NSTTs
can be answered efficiently.
We present a new polynomial time algorithm in RPNI-style
that learns monadic queries defined by deterministic NSTTs from
completely annotated examples, where all selected nodes are
distinguished.
In practice, users prefer to provide partial annotations. We
resolve this by intelligent tree pruning heuristics. We introduce
pruning NSTTs - a formalism that shares many advantages of NSTTs.
This leads us to an interactive learning algorithm for monadic
queries defined by pruning NSTTs, which satisfies a new formal
active learning model in the style of Angluin (1987).
We have implemented our interactive learning algorithm
and integrated it into a visually interactive Web information
extraction system -- called Squirrel -- by plugging it into
the Mozilla Web browser. Experiments on realistic Web documents confirm
excellent quality with very few user interactions
during wrapper induction.
},
pages = "33--67",
month = "January",
volume = "66",
number = "1",
url = {http://hal.inria.fr/inria-00087226/en},
auteur = {MOSTRARE JulienCarme RemiGilleron JoachimNiehren AurelienLemay TRALALA ACIMDD STC GRAPPA Hal:6@18qm Query XML},
}
@Article{ChampavereGilleronLemay09,
audience = \{Art1},
author = {Jérôme Champavère and Rémi Gilleron and Aurélien Lemay and Joachim Niehren},
title = {Efficient Inclusion Checking for Deterministic Tree Automata and {XML} Schemas},
journal = ICOMP,
year = {2009},
volume = {207},
number = {11},
pages = {1181--1208},
month = {november},
note = {doi:10.1016/j.ic.2009.03.003},
url = {http://hal.inria.fr/inria-00366082/en},
auteur = {Mostrare Codex},
abstract = {We present algorithms for testing language inclusion L(A) ⊆ L(B) between tree automata in time O(|A| · |B|) where B is deterministic (bottom-up or top-down). We extend our algorithms for testing inclusion of automata for unranked trees A in deterministic DTDs or deterministic EDTDs with re- strained competition D in time O(|A| · |Σ| · |D|). Previous algorithms were less efficient or less general.},
}
@Article{EggKollerNiehren01,
author = {Markus Egg and Alexander Koller and Joachim Niehren},
title = {The Constraint Language for Lambda Structures},
journal = JoLLI,
year = {2001},
audience = \{Art1},
pages = {457-485},
url = {http://www.ps.uni-sb.de/Papers/abstracts/clls2000.html},
abstract = {This paper presents the Constraint Language for Lambda Structures (CLLS), a first-order language for semantic underspecification that
conservatively extends dominance constraints. It is interpreted over
lambda structures, tree-like structures that encode lambda-terms. Based on
CLLS, we present an underspecified, uniform analysis of scope,
ellipsis, anaphora, and their interactions. CLLS solves a variable
capturing problem that is omnipresent in scope underspecification and
can be processed efficiently.},
volume = {10},
}
@Article{ErkKollerNiehren02,
journal = JRLC,
year = {2002},
author = {Katrin Erk and Alexander Koller and Joachim Niehren},
title = {Processing Underspecified Semantic Representations in the Constraint Language for Lambda Structures},
audience = \{Art1},
number = "1",
pages = {127--169},
url = {http://www.ps.uni-sb.de/Papers/abstracts/processing00.html},
abstract = {The constraint language for lambda structures (CLLS) is an expressive language of tree descriptions which combines
dominance constraints with powerful parallelism and binding
constraints. CLLS was introduced as a uniform framework for defining
underspecified semantics representations of natural language
sentences, covering scope, ellipsis, and anaphora. This article
presents saturation-based algorithms for processing the complete
language of CLLS. It also gives an overview of previous results on
questions of processing and complexity.},
volume = "1",
}
@Article{ErkNiehren07,
journal = IPL,
year = 2007,
author = {Katrin Erk and Joachim Niehren},
title = {Dominance Constraints in Stratified Context Unification},
audience = \{Art1},
number = 4,
pages = {141-147},
month = feb,
url = {http://hal.inria.fr/inria-00094787/en},
auteur = {MOSTRARE GRAPPA HAL:snzw0vap STC Query},
abstract = {We express dominance constraints in the once-only nesting fragment of stratified context unification, which therefore is NP-complete.},
volume = 101,
}
@Article{GauwinNiehrenRoos08,
author = {Olivier Gauwin and Joachim Niehren and Yves Roos},
title = {Streaming Tree Automata},
journal = IPL,
year = {2008},
audience = \{Art1},
number = 1,
pages = {13-17},
month = dec,
url = {http://hal.inria.fr/inria-00288445/en},
auteur = {MOSTRARE Codex ENUM},
abstract = {Streaming validation and querying of XML documents
are often based on automata for tree-like structures.
We propose a new notion of streaming tree automata
in order to unify the two main approaches, which have not been
linked so far: automata for nested words or equivalently visibly
pushdown automata, and respectively pushdown forest automata.
},
volume = 109,
}
@Article{GauwinNiehrenTison10,
audience = \{Art1},
journal = ICOMP,
year = 2010,
title = {Queries on XML Streams with Bounded Delay and Concurrency},
author = {Olivier Gauwin and Joachim Niehren and Sophie Tison},
abstract = {Query answering algorithms on XML streams check answer candidates on the fly in order to avoid the unnecessary buffering whenever possible. The delay and concurrency of a query are two measures for the degree of their streamability. They count the maximal number of stream elements during the life time for some query answer, and respectively, the maximal number of simultaneously alive answer candidates of a query. We study queries defined by deterministic nested word automata, which subsume large streamable fragments of XPath subject to schema restrictions by DTDs modulo P-time translations. We show that bounded and k-bounded delay and concurrency of such automata-defined queries are all decidable in polynomial time in the size of the automaton. Our results are obtained by P-time reduction to the bounded valuedness problem for recognizable relations between unranked trees, a problem that we show to be decidable in P-time.},
annote = {accepted for publication},
auteur = {Mostrare ENUM Codex},
url = {http://www.grappa.univ-lille3.fr/~niehren/Papers/delay/0.pdf},
}
@Article{JohnLhoussaineNiehren09b,
author = {Mathias John and Cédric Lhoussaine and Joachim Niehren and Adelinde Uhrmacher},
title = {The Attributed Pi Calculus with Priorities},
journal = TCSB,
year = 2010,
audience = \{Art1},
number = {{XII}},
pages = {13-76},
url = {http://hal.archives-ouvertes.fr/inria-00422969/en/},
auteur = {BioComputing Mostrare},
abstract = {The attributed pi calculus (pi(L)) forms an extension of the pi calculus with attributed processes and attribute dependent synchronization. To ensure flexibility, the calculus is parametrized with the language L which defines possible values of attributes. pi(L) can express polyadic synchronization as in pi@ and thus diverse compartment organizations. A non-deterministic and a stochastic semantics, where rates may depend on attribute values, is introduced. The stochastic semantics is based on continuous time Markov chains. A simulation algorithm is developed which is firmly rooted in this stochastic semantics. Two examples, the movement processes in the phototaxis of Euglena and the cooperative binding in the gene regulation of the lambda Phage, underline the applicability of pi(L) to systems biology.},
volume = 5945,
}
@Article{KollerNiehrenStriegnitz2000,
author = {Alexander Koller and Joachim Niehren and Kristina Striegnitz},
title = {Relaxing Underspecified Semantic Representations for Reinterpretation},
journal = Grammars,
audience = \{Art1},
year = {2000},
note = {Special Issue on {MOL}'99.},
url = {http://www.ps.uni-sb.de/Papers/abstracts/relax2000.html},
abstract = {Type and sort conflicts in semantics are usually resolved by a process of reinterpretation, which introduces an
operator into the semantic representation. We elaborate on the
foundations of a recent approach to reinterpretation within a
framework for semantic underspecification. In this approach, relaxed
underspecified semantic representations are inferred from the
syntactic structure, leaving space for subsequent addition of
reinterpretation operators. Unfortunately, a structural danger
of overgeneration is inherent to the relaxation of underspecified
semantic representations. We identify the problem and distinguish
structural properties that avoid it. We furthermore develop
techniques for proving these properties and apply them to
prove the safety of relaxation in a prototypical
syntax/semantics interface. In doing so, we present some novel
properties of tree descriptions in the constraint
language over lambda structures (CLLS).},
volume = {3},
number = {2/3},
pages = {217-241},
}
@Article{KuttlerNiehren06,
author = {Céline Kuttler and Joachim Niehren},
title = {Gene Regulation in the Pi Calculus: Simulating Cooperativity at the Lambda Switch},
year = {2006},
audience = \{Art1},
journal = TCSB,
month = nov,
annote = {Special issue on 2nd International Workshop on Concurrent Models in Molecular Biology (BioConcur 2004).},
url = {http://hal.archives-ouvertes.fr/inria-00089218/en},
auteur = {MOSTRARE STC GRAPPA BIOCOMPUTING HAL:g548u3},
volume = 4220,
number = {{VII}},
pages = {24-55},
}
@Article{MartensNiehren07,
author = {Wim Martens and Joachim Niehren},
title = {On the Minimization of {XML} Schemas and Tree Automata for Unranked Trees},
journal = JCSS,
year = {2007},
audience = \{Art1},
number = 4,
pages = {550-583},
annote = {{Special issue of {DBLP} 05}},
url = {http://hal.inria.fr/inria-00088406/en},
auteur = {MOSTRARE GRAPPA TRALALA ACIMDD STC HAl:0?n97nwz Query},
abstract = {
Automata for unranked trees form a foundation for XML schemas,
querying and pattern languages. We study the problem of
efficiently minimizing such automata.
First, we study unranked tree automata that are standard in
database theory, assuming bottom-up determinism and that
horizontal recursion is represented by deterministic finite
automata. We show that minimal automata in that class are not
unique and that minimization is NP complete.
Second, we study more recent automata classes that do
allow for polynomial time minimization. Among those, we show that
bottom-up deterministic stepwise tree automata yield the most
succinct representations.
Third, we investigate abstractions of ML schema languages. In particular, we show that the class of one-pass preorder typable schemas allows for polynomial time minimization and unique minimal models. },
volume = 73,
}
@Article{MuellerNiehren00,
author = {Martin Müller and Joachim Niehren},
title = {Ordering Constraints over Feature Trees Expressed in Second-order Monadic Logic},
journal = ICOMP,
year = {2000},
audience = \{Art1},
number = {1/2},
pages = {22--58},
note = {Special Issue on {RTA} 1998.},
url = {http://www.ps.uni-sb.de/Papers/abstracts/SWSJournal99.html},
abstract = {The system FT
of ordering constraints over feature trees has
been introduced as an extension of the system FT of equality
constraints over feature trees. While the first-order theory of FT
is well understood, only few complexity and decidability results are
known for fragments of the first-order theory of
FT${}_leq$.
We
introduce a new handle for such decidability questions by
showing how to express ordering constraints over feature trees in
second-order monadic logic (S2S or WS2S). Our relationship implies
a new decidability
result for feature logics, namely that the entailment problem of
FT${}_leq$
with existential quantifiers
$phi_1models exists x_1ldotsexists x_n phi_2$
is decidable. We also show that
this problem is PSPACE-hard even though the quantifier-free case can
be solved in cubic time. To our knowledge, this is the first time
that a non-trivial decidability result of feature logic is reduced
to Rabins famous tree theorem.},
volume = {159},
}
@Article{MuellerNiehrenPodelski00,
author = {Martin Müller and Joachim Niehren and Andreas Podelski},
title = {Ordering Constraints over Feature Trees},
journal = CIJ,
year = {2000},
audience = \{Art1},
number = {1--2},
pages = {7--42},
month = jan,
note = {Special Issue on {CP}'97, Linz, Austria.},
url = {http://www.ps.uni-sb.de/Papers/abstracts/ftsub-constraints-99.html},
abstract = {Feature trees are the formal basis for algorithms manipulating record like structures in constraint programming,
computational linguistics and in concrete applications like software
configuration management. Feature trees model records, and
constraints over feature trees yield extensible and modular record
descriptions. We introduce the constraint system
FT$leq$ of
ordering constraints interpreted over feature trees. Under the view
that
feature trees represent symbolic information, the relation
$leq$
corresponds to the information ordering (``carries less information
than''). We present two algorithms in cubic time, one for the
satisfiability problem and one for the entailment problem of
FT${}_leq$.
We show that
FT${}_leq$
has the independence property. We are thus able
to handle negative conjuncts via entailment and obtain a cubic
algorithm that decides the satisfiability of conjunctions of
positive and negated ordering constraints over feature trees.
Furthermore, we reduce the satisfiability problem of D{"o}rre's weak
subsumption constraints to the satisfiability problem of
FT${}_leq$ and
improve the complexity bound for solving weak subsumption
constraints from $O(n^5)$ to $O(n^3)$.},
volume = {5},
}
@Article{MuellerNiehrenTreinen01,
audience = \{Art1},
author = {Martin Müller and Joachim Niehren and Ralf Treinen},
title = {The First-Order Theory of Ordering Constraints over Feature Trees},
journal = DMTCS,
year = {2001},
pages = {193-234},
url = {http://www.ps.uni-sb.de/Papers/abstracts/FTSubTheory-Long:99.html},
volume = "4",
number = "2",
abstract = {The system FT$_\leq$ of ordering constraints over feature trees has been introduced as an extension of
the system FT of equality constraints over
feature trees. We investigate the first-order theory of FT$_\leq$
and its fragments in detail, both over
finite trees and over possibly infinite trees. We prove that the
first-order theory of FT$_\leq$ is
undecidable, in contrast to the first-order theory of FT which
is well-known to be decidable. We show
that the entailment problem of FT$_\leq$
with existential quantification is PSPACE-complete. So far, this
problem has been shown decidable, coNP-hard in case of finite trees,
PSPACE-hard in case of arbitrary trees, and cubic time when restricted
to quantifier-free entailment judgments. To show PSPACE-completeness,
we show that the entailment problem of FT$_\leq$ with existential
quantification is equivalent to the
inclusion problem of non-deterministic finite automata.},
}
@Article{Niehren00,
author = {Joachim Niehren},
title = {Uniform Confluence in Concurrent Computation},
journal = JFP,
year = {2000},
audience = \{Art1},
number = 5,
pages = {453-499},
month = sep,
url = {http://www.ps.uni-sb.de/Papers/abstracts/Uniform:2000.html},
abstract = {Indeterminism is typical for concurrent computation. If several concurrent actors compete for the same resource then at most one of them may
succeed, whereby the choice of the successful actor is indeterministic. As a consequence, the execution of a concurrent program may be
nonconfluent. Even worse, most observables (termination, computational result, and time complexity) typically depend on the scheduling of
actors created during program execution. This property contrast concurrent programs from purely functional programs. A functional program is
uniformly confluent in the sense that all its possible executions coincide modulo reordering of execution steps. In this paper, we investigate
concurrent programs that are uniformly confluent and their relation to eager and lazy functional programs.
We study uniform confluence in concurrent computation within the applicative core of the pi-calculus which is widely used in different models of
concurrent programming (with interleaving semantics). In particular, the applicative core of the pi-calculus serves as a kernel in foundations of
concurrent constraint programming with first-class procedures (as provided by the programming language Oz). We model eager functional
programming in the lambda-calculus with weak call-by-value reduction and lazy functional programming in the call-by-need lambda-calculus with standard
reduction. As a measure of time complexity, we count application steps. We encode the lambda-calculus with both above reduction strategies into the
applicative core of the pi-calculus and show that time complexity is preserved. Our correctness proofs employs a new technique based on
uniform confluence and simulations. The strength of our technique is illustrated by proving a folk theorem, namely that the call-by-need
complexity of a functional program is smaller than its call-by-value complexity.
The unabridged version of this article is available from Uniform:99. Due to lack of space, the journal version does not contain the encoding of the
delta-calculus (introduced in the paper) into the applicative core of the pi-calculus which is of its own interest.
},
volume = 10,
}
@Article{NiehrenPriesnitz03,
title = {Non-Structural Subtype Entailment in Automata Theory},
journal = ICOMP,
year = "2003",
audience = \{Art1},
author = {Joachim Niehren and Tim Priesnitz},
url = {http://www.ps.uni-sb.de/Papers/abstracts/subtype.html},
abstract = {Decidability of non-structural subtype entailment is a long-standing open problem in programming language
theory. In this paper, we apply automata theoretic
methods to characterize the problem equivalently
by using regular expressions and word equations.
This characterization induces new results on
non-structural subtype entailment, constitutes
a promising starting point for further investigations
on decidability, and explains for the first time
why the problem is so difficult. The difficulty
is caused by implicit word equations that we make
explicit.},
auteur = {MOSTRARE STC GRAPPA},
volume = 169,
number = "2",
pages = {319-354},
month = nov,
}
@Article{NiehrenSchwinghammerSmolka06,
author = {Joachim Niehren and Jan Schwinghammer and Gert Smolka},
title = {A Concurrent Lambda Calculus with Futures},
journal = TCS,
year = {2006},
audience = \{Art1},
number = 3,
pages = {338-356},
month = nov,
url = {http://hal.inria.fr/inria-00090434/en},
auteur = {{MOSTRARE TRALALA GRAPPA STC ACIMDD}},
abstract = {
We introduce a new concurrent lambda calculus with futures,
lambda(fut), to model the operational semantics of Alice, a
concurrent extension of ML. lambda(fut) is a minimalist
extension of the call-by-value lambda-calculus that yields
the full expressiveness to define, combine, and implement
a variety of standard concurrency constructs such as channels,
semaphores, and ports. We present a linear type system for
lambda(fut) by which the safety of such definitions
and their combinations can be proved:
Well-typed implementations cannot be corrupted in any well-typed context.
},
volume = 364,
}
@Article{NiehrenTreinenTison00,
author = {Joachim Niehren and Ralf Treinen and Sophie Tison},
title = {On Rewrite Constraints and Context Unification},
journal = IPL,
year = {2000},
audience = \{Art1},
number = {1-2},
pages = {35--40},
month = apr,
url = {http://www.ps.uni-sb.de/Papers/abstracts/rewrite-context.html},
abstract = {We show that stratified context unification, which is one of the
most expressive fragments of context unification known to be
decidable, is equivalent to the satisfiability problem of slightly
generalized rewriting constraints.},
volume = {74},
}
%========================== InProceedings ==========================
@InProceedings{AlthausDuchierKollerMehlhornNiehrenThiel01,
author = {Ernst Althaus and Denys Duchier and Alexander Koller and Kurt Mehlhorn and Joachim Niehren and Sven Thiel},
title = {An Efficient Algorithm for the Configuration Problem of Dominance Graphs},
booktitle = {Proceedings of the 12th ACM-SIAM Symposium on Discrete Algorithms},
audience = \{Com1},
url = {http://www.ps.uni-sb.de/Papers/abstracts/dom-graph.html},
abstract = {Dominance constraints are logical tree descriptions originating from automata theory that have multiple applications in computational
linguistics. The satisfiability problem of dominance constraints is
NP-complete. In most applications, however, only \emph{normal}
dominance constraints are used. The satisfiability problem of normal
dominance constraints can be reduced in linear time to the configuration
problem of dominance graphs, as shown recently. In this paper,
we give a polynomial time algorithm testing configurability of dominance
graphs (and thus satisfiability of normal dominance constraints).
Previous to our work no polynomial time algorithms were known.},
month = jan,
pages = {815--824},
publisher = ACM,
year = {2001},
address = {Washington, DC},
}
@InProceedings{BodirskyDuchierMieleNiehren04,
title = {A New Algorithm for Normal Dominance Constraints},
booktitle = {{{ACM-SIAM} Symposium on Discrete Algorithms}},
audience = \{Com1},
author = {Manuel Bodirsky and Denys Duchier and Sebastian Miele and Joachim Niehren},
publisher = ACM,
url = {http://www.ps.uni-sb.de/Papers/abstracts/wndc.pdf},
abstract = {Dominance constraints are logical descriptions of trees. Efficient
algorithms for the subclass of normal dominance constraints were recently proposed. We present a new and simpler graph algorithm
solving these constraints more efficiently, in quadratic time per
solved form. It also applies to weakly normal dominance constraints
as needed for an application to computational linguistics.
Subquadratic running time can be achieved employing decremental
graph biconnectivity algorithms.},
auteur = {MOSTRARE ACIMDD GRAPPA STC Query},
pages = {54-78},
year = {2004},
month = jan,
}
@InProceedings{BodirskyErkKollerNiehren01,
author = {Manuel Bodirsky and Katrin E. Erk and Alexander Koller and Joachim Niehren},
booktitle = {International Conference on Rewriting Techniques and Applications},
audience = \{Com1},
title = {Beta Reduction Constraints},
publisher = {Springer-Verlag, Berlin},
month = may,
address = {Utrecht, The Netherlands},
pages = {31-46},
abstract = {The constraint language for lambda structures (CLLS) can model lambda terms that are known only partially.
In this paper, we introduce beta reduction constraints
to describe beta reduction steps between partially known
lambda terms. We show that beta reduction constraints can
be expressed in an extension of CLLS by group
parallelism. We then extend a known semi-decision
procedure for CLLS to also deal with group parallelism
and thus with beta-reduction constraints.},
url = {http://www.ps.uni-sb.de/Papers/abstracts/beta.html},
year = {2001},
series = {Lecture Notes in Computer Science},
editor = {Aart Middeldorp},
}
@InProceedings{BodirskyErkKollerNiehren01b,
audience = \{Com1},
author = {Manuel Bodirsky and Katrin Erk and Alexander Koller and Joachim Niehren},
title = {Underspecified Beta Reduction},
booktitle = {39th Annual Meeting of the Association for Computational Linguistics},
url = {http://www.ps.uni-sb.de/Papers/abstracts/usp-beta.html},
abstract = {For ambiguous sentences, traditional semantics construction produces large numbers of higher-order formulas,
which must then be beta-reduced individually. Underspecified
versions can produce compact descriptions of all readings, but
it is not known how to perform beta reduction on these
descriptions. We show how to do this using beta reduction
constraints in the constraint language for lambda-structures
(CLLS).},
pages = {74-81},
year = {2001},
address = {Toulouse, France},
month = jul,
}
@InProceedings{CarmeLemayNiehren2004,
booktitle = {7th International Colloquium on Grammatical Inference},
title = "Learning Node Selecting Tree Transducer from Completely Annotated Examples",
audience = \{Com1},
author = {Julien Carme and Aurélien Lemay and Joachim Niehren},
series = LNAI,
publisher = SV,
url = {http://www.grappa.univ-lille3.fr/~lemay/publi/icgi04.pdf},
abstract = {Web documents in HTML or XML form trees with nodes containing text.
A base problem in Web information extraction is to find
appropriate queries for informative nodes in trees. We propose to learn queries
for nodes in trees automatically from examples. We introduce node selecting tree transducer
(NSTT) for representing node queries in trees and show how to induce determinist
ic NSTTs
in polynomial time from completely annotated examples by methods of grammatical
inference.
We have implemented learning algorithms for NSTTs, started applying them to
Web information extraction, and present first experimental results.}
,
auteur = {JulienCarme AurelienLemay JoachimNiehren MOSTRARE STC GRAPPA ACIMDD},
pages = "91--102",
year = "2004",
volume = 3264,
}
@InProceedings{CarmeNiehrenTommasi04,
author = {Julien Carme and Joachim Niehren and Marc Tommasi},
title = {Querying Unranked Trees with Stepwise Tree Automata},
booktitle = {19th International Conference on Rewriting Techniques and Applications},
audience = \{Com1},
year = "2004",
volume = "3091",
series = LNCS,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/stepwise.html},
auteur = {JulienCarme JoachimNiehren MarcTommasi MOSTRARE STC GRAPPA ACIMDD},
abstract = {The problem of selecting nodes in unranked trees is
the most basic querying problem for XML. We propose
stepwise tree automata for querying unranked trees.
Stepwise tree automata can express the same monadic
queries as monadic Datalog and monadic second-order logic.
We prove this result by reduction to the ranked case, via a
new systematic correspondence that relates unranked
and ranked queries.},
pages = "105--118",
}
@InProceedings{ChampavereGilleronLemay08,
audience = \{Com1},
author = {Jérôme Champavère and Rémi Gilleron and Aurélien Lemay and Joachim Niehren},
title = {Efficient Inclusion Checking for Deterministic Tree Automata and {DTDs}},
booktitle = {2nd International Conference on Language and Automata Theory and Applications},
year = {2008},
url = {http://hal.inria.fr/inria-00192329/fr/},
series = LNCS,
publisher = SV,
annote = {An extended version is available at http://www.grappa.univ-lille3.fr/~champavere/Recherche/publications/CGLN08EIC.extended.pdf} ,
volume = {5196},
auteur = {{MOSTRARE STC GRAPPA Tralala}},
abstract = { We present a new algorithm for testing
language inclusion L(A) subset L(B) between
tree automata in time O(|A|*|B|) where B is deterministic. We
extend this algorithm for testing inclusion between
automata for unranked trees A and deterministic DTDs D
in time O(|A|*|Sigma|*|D|). No previous
algorithms with these complexities exist.
},
pages = {184--195},
}
@InProceedings{ChampavereGilleronLemay08a,
author = {Jérôme Champavère and Rémi Gilleron and Aurélien Lemay and Joachim Niehren},
title = {{Schema-Guided Induction of Monadic Queries}},
booktitle = {9th International Colloquium
on Grammatical Inference},
audience = \{Com1},
year = 2008,
volume = {5278},
series = LNCS,
publisher = SV,
url = {http://hal.inria.fr/inria-00309408/en/},
auteur = {MOSTRARE STC GRAPPA Tralala Transduce},
abstract = {The induction of monadic node selecting queries from partially annotated XML-trees is a key task in Web information extraction. We show how to integrate schema guidance into an RPNI-based learning algorithm, in which monadic queries are represented by pruning node selecting tree transducers. We present experimental results on schema guidance by the DTD of HTML.},
pages = {15-28},
}
@InProceedings{DebusmannDuchierNiehren04,
author = {Ralph Debusmann and Denys Duchier and Joachim Niehren},
title = {The {XDG} Grammar Development Kit},
booktitle = {2nd International Conference on Multiparadigm Programming in {Mozart/Oz}},
audience = \{Com1},
year = {2004},
volume = {3389},
series = LNAI,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/moz04},
auteur = {JoachimNiehren STC GRAPPA MOSTRARE},
abstract = {Extensible dependency grammar (XDG) is a graph description language,
whose formulas can be solved by constraint programming. XDG yields a
declarative approach to natural language processing for parsing and
generation. In this paper, we present the XDG development kit,
the first XDG-based grammar development system, which we implemented
in Mozart/Oz. This includes an expressive lexicon specification
language not published previously.},
pages = {190--201},
}
@InProceedings{DuchierNiehren00,
booktitle = {Proceedings of the First International Conference on Computational Logic (CL2000)},
title = {Dominance Constraints with Set Operators},
audience = \{Com1},
author = {Denys Duchier and Joachim Niehren},
month = jul,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/dombool.html},
abstract = {Dominance constraints are widely used in computational linguistics as a language for talking and
reasoning about trees. In this paper, we extend dominance
constraints by admitting
set operators. Set operators contribute
a controlled form of disjunction that is emminently well-suited for
constraint propagation. We present a solver for dominance
constraints with set operators as a system of abstract
propagation and distribution rules, and prove its soundness
and completeness. We then
derive an efficient implementation in a constraint programming
language with finite sets and prove its
faithfullness to the abstract inference rules.},
volume = 1861,
pages = {326-341},
year = {2000},
series = LNCS,
}
@InProceedings{EggNiehrenRuhrbergXu98,
audience = \{Com1},
author = {Markus Egg and Joachim Niehren and Peter Ruhrberg and Feiyu Xu},
title = {Constraints over Lambda-Structures in Semantic Underspecification},
booktitle = {Joined 17th International Conference on Computational Linguistics and 36th Annual Meeting
of the Association for Computational Linguistics
(COLING/ACL'98)},
abstract = {We introduce a first-order language for semantic underspecification that we call Constraint Language for
Lambda-Structures (CLLS). A lambda-structure can be
considered as a lambda-term up to consistent renaming
of bound variables (alpha-equality);
a constraint of CLLS is an underspecified description of a
$lambda$-structure. CLLS solves a capturing problem
omnipresent in underspecified scope representations.
CLLS features constraints for dominance,
lambda binding, parallelism, and anaphoric links. Based on
CLLS we present a simple, integrated, and underspecified
treatment of scope, parallelism, and anaphora.},
address = {Montreal, Canada},
pages = {353--359},
month = aug,
url = {http://www.ps.uni-sb.de/Papers/abstracts/CLLS-98.html},
year = {1998},
}
@InProceedings{ErkNiehren00,
author = {Katrin E. Erk and Joachim Niehren},
title = {Parallelism Constraints},
booktitle = {International Conference on Rewriting Techniques and Applications},
audience = \{Com1},
year = {2000},
volume = {1833},
series = LNCS,
address = {Norwich, U.K.},
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/parallelism.html},
abstract = {Parallelism constraints are logical desciptions of trees. They are as expressive as context unification, i.e.
second-order linear unification. We present
a semi-decision procedure enumerating all most general
unifiers of a parallelism constraint and prove it sound
and complete. In contrast to all known procedures
for context unification, the presented procedure
terminates for the important fragment of dominance
constraints and performs reasonably well in a recent
application to underspecified natural language semantics.},
pages = {110--126},
}
@InProceedings{ErkNiehren03,
booktitle = {11th Conference of the European Chapter of the Association of Computational Linguistics},
audience = \{Com1},
title = {Well-Nested Parallelism Constraints for Ellipsis Resolution},
author = {Katrin Erk and Joachim Niehren},
organization = {Association for Compuational Linguistics},
url = {http://www.ps.uni-sb.de/Papers/abstracts/wellnested.html},
abstract = {The Constraint Language for Lambda Structures (CLLS) is an expressive tree description language. It provides a uniform framework for underspecified semantics, covering scope,
ellipsis, and anaphora. Efficient algorithms exist for the sublanguage that models scope. But so far no terminating algorithm exists for sublanguages that model ellipsis. We
introduce well-nested parallelism constraints and show that they solve this problem.},
month = apr,
auteur = {MOSTRARE GRAPPA STC},
key = {a003},
pages = {115--122},
year = {2003},
}
@InProceedings{FiliotNiehrenTalbotTison07,
author = {Emmanuel Filiot and Joachim Niehren and Jean-Marc Talbot and Sophie Tison},
title = {Polynomial Time Fragments of {XPath} with Variables},
booktitle = {26th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems},
audience = \{Com1},
year = {2007},
publisher = ACM,
url = {http://hal.inria.fr/inria-00135678},
auteur = {MOSTRARE STC TRALALA GRAPPA Query
Hal:pb1q9n ENUM XML},
abstract = {
Variables in XPath 2.0 are fundamental for selecting
n-tuples of nodes in trees. The navigational core of XPath
2.0 is known to capture first-order (FO) logic while being
PSPACE complete with respect to model checking. In this paper,
we distinguish a fragment of Core XPath 2.0 that we call the
polynomial-time path language (PPL). We show that
PPL remains FO-complete even though enjoying
polynomial time query answering (and thus model checking).
},
pages = {205-214},
}
@InProceedings{FuchssKollerNiehrenThater04,
title = {Minimal Recursion Semantics as Dominance Constraints: Translation, Evaluation, and Analysis},
booktitle = {{42th Meeting of the Association for Computational Linguistics}},
audience = \{Com1},
author = {Ruth Fuchss and Alexander Koller and Joachim Niehren and Stefan Thater},
month = jul,
url = {http://www.ps.uni-sb.de/Papers/abstracts/mrs_eval.html},
auteur = {MOSTRARE GRAPPA ACIMDD STC},
abstract = {We show that a practical translation of MRS descriptions into normal
dominance constraints is feasible. We start from a recent theoretical
translation, develop it into a practical system, and apply it to the
output of the English Resource Grammar (ERG) on the Redwoods corpus.
We validate the assumptions made by the theoretical translation for a
large majority of cases; the MRS descriptions computed in all other
cases seem to be systematically incomplete.
},
pages = {247-254},
year = {2004},
}
@InProceedings{GauwinNiehrenTison09a,
booktitle = {3rd International Conference on Language
and Automata Theory and Applications},
title = {Bounded Delay and Concurrency for Earliest Query Answering},
author = {Olivier Gauwin and Joachim Niehren and Sophie Tison},
audience = \{Com1},
volume = {5457},
series = LNCS,
publisher = SV,
abstract = {Earliest query answering is an important objective of
recent XML streaming algorithms. Given a stream of events produced
by a preorder traversal over an XML tree, and a node
selection query, the problem is to compute answer nodes
online so that the delay between node traversal
and selection is minimized. Furthermore, the algorithm
should remove failed answer candidates as early as possible.
Queries tractable for streaming should satisfy two properties:
bounded delay for node selection and
a bounded number of concurrently alive answer candidates. We show that
both properties are decidable for $n$-ary MSO-definable queries. As
proof technique we develop and apply the theory of tree automata
recognizable relations between unranked trees.},
pages = {350-361},
url = {http://hal.inria.fr/inria-00348463/en},
year = 2009,
auteur = {Mostrare Grappa ENUM},
}
@InProceedings{GauwinNiehrenTison09b,
author = {Olivier Gauwin and Joachim Niehren and Sophie Tison},
title = {Earliest Query Answering for Deterministic Nested Word Automata},
booktitle = {17th International Symposium on Fundamentals of Computer Theory},
audience = \{Com1},
auteur = {Mostrare Codex ENUM},
url = {http://hal.inria.fr/inria-00390236/en},
abstract = { Earliest query answering (EQA) is an objective of many recent streaming algorithms for XML query answering, that aim for close to optimal memory management. In this paper, we show that EQA is infeasible even for a small fragment of Forward XPath except if P=NP. We then present an EQA algorithm for queries and schemas defined by deterministic nested word automata (dNWAs) and distinguish a large class of dNWAs for which streaming query answering is feasible in polynomial space and time.},
publisher = SV,
pages = {121--132},
year = {2009},
volume = {5699},
series = LNCS,
}
@InProceedings{JohnLhoussaineNiehren08,
title = {The Attributed Pi Calculus},
booktitle = {Computational Methods in Systems Biology, 6th International Conference},
audience = \{Com1},
author = {Mathias John and Cédric Lhoussaine and Joachim Niehren and Adelinde Uhrmacher},
abstract = {We introduce the attributed pi-calculus, an extension of
the pi-calculus with attributed processes and attribute
dependent synchronization. Attribute values are useful to define spatial, geometrical,
physical, or biological properties of processes.
We show that the attributed pi-calculus
can express poly-synchronization as in pi@
and thus all kinds of compartment organizations. It equally subsumes
Spico's pattern-synchronization, the basic concept needed for
defining concurrent objects in the pi-calculus. We provide a stochastic
semantics, where the rates may depend on attribute values, and
the corresponding simulation algorithm. This turns the attributed
pi-calculus into a highly expressive modeling language for systems biology.
},
auteur = {Mostrare Grappa STC BioComputing},
publisher = SV,
series = LNCS,
url = {http://hal.archives-ouvertes.fr/inria-00308970/en/},
pages = {83-102},
year = {2008},
volume = {5307},
}
@InProceedings{JohnLhoussaineNiehren09,
audience = \{Com1},
booktitle = {Computational Methods in Systems Biology, 7th International Conference},
author = {Mathias John and Cédric Lhoussaine and Joachim Niehren},
title = {Dynamic Compartments in the Imperative Pi Calculus},
pages = {235-250},
volume = 5688,
url = {http://hal.archives-ouvertes.fr/inria-00422970/en},
series = LNCS,
auteur = {BioComputing Mostrare},
abstract = {Dynamic compartments with mutable configurations and variable volumes are of basic interest for the stochastic modeling of biochemistry in cells. We propose a new language to express dynamic compartments that we call the imperative π-calculus. It is obtained from the attributed π-calculus by adding imperative assignment operations to a global store. Previous approaches to dynamic compartments are improved in flexibility or efficiency. This is illustrated by an appropriate model of osmosis and a correct encoding of BioAmbients.}
,
year = {2009},
publisher = SV,
}
@InProceedings{KollerMehlhornNiehren00,
author = {Alexander Koller and Kurt Mehlhorn and Joachim Niehren},
title = {A Polynomial-Time Fragment of Dominance Constraints},
booktitle = {38th Annual Meeting of the Association of Computational Linguistics},
audience = \{Com1},
year = {2000},
address = {Hong Kong},
month = "3--6"#oct,
url = {http://www.ps.uni-sb.de/Papers/abstracts/poly-dom.html},
abstract = {Dominance constraints are a logical language for describing trees that is widely used in
computational linguistics. Their general satisfiability
problem is known to be NP-complete. Here we identify
emph{normal} dominance constraints, a natural
fragment whose satisfiability problem we show to be in polynomial
time. We present a quadratic satisfiability algorithm and use it in
another algorithm that enumerates solutions efficiently. Our result is
useful for various applications of dominance constraints and related
formalisms.},
pages = {368--375},
}
@InProceedings{KollerNiehren00,
author = {Alexander Koller and Joachim Niehren},
title = {On Underspecified Processing of Dynamic Semantics},
booktitle = {18th International Conference on Computational Linguistics},
audience = \{Com1},
year = {2000},
address = {Saarbr{"u}cken, Germany},
month = jul#{ 31 -- }#aug#{ 4},
url = {http://www.ps.uni-sb.de/Papers/abstracts/dynamic.html},
abstract = {We propose a new inference system which operates on underspecified semantic representations of scope and anaphora. This
inference system exploits anaphoric accessibility conditions known
from dynamic semantics to decide scope ambiguities if possible. The
main feature of the system is that it deals with underspecified
descriptions directly, i.e. without enumerating readings.},
pages = {460--466},
}
@InProceedings{KollerNiehrenStriegnitz99,
author = {Alexander Koller and Joachim Niehren and Kristina Striegnitz},
title = {Relaxing Underspecified Semantic Representations for Reinterpretation},
booktitle = {6th Meeting on Mathematics of Language},
audience = \{Com1},
year = {1999},
address = {Orlando, Florida},
month = {jul},
url = {http://www.ps.uni-sb.de/Papers/abstracts/relax2000.html},
abstract = {Type and sort conflicts in semantics are usually resolved by a process of reinterpretation. Recently, Egg (1999) has proposed an
alternative account in which conflicts are avoided by
underspecification. The main idea is to derive sufficiently relaxed
underspecified semantic representations; addition of reinterpretation
operators then simply is further specialization. But in principle,
relaxing underspecified representations bears the danger of
overgeneration. In this paper, we investigate this problem in the
framework of CLLS, where underspecified representations are expressed
by tree descriptions subsuming dominance constraints. We introduce
some novel properties of dominance constraints and present a safety
criterion that ensures that an underspecified description can be
relaxed without adding unwanted readings. We then apply this criterion
systematically to Egg's analysis and show why its relaxation operation
does not lead to overgeneration.},
pages = {74--87},
}
@InProceedings{KollerNiehrenThater03,
audience = \{Com1},
author = {Alexander Koller and Joachim Niehren and Stefan Thater},
title = {Bridging the Gap Between Underspecification Formalisms: Hole Semantics as Dominance Constraints},
booktitle = {Meeting of the European Chapter of the Association of Computational Linguistics},
abstract = {We define a back-and-forth translation between Hole Semantics and
dominance constraints, two formalisms used in underspecified
semantics. There are fundamental differences between the two, but we
show that they disappear on practically useful descriptions. Our
encoding bridges a gap between two underspecification formalisms, and
speeds up the processing of Hole Semantics.},
pages = {195-202},
url = {http://www.ps.uni-sb.de/Papers/abstracts/holes-dom.html},
year = {2003},
month = apr,
auteur = {MOSTRARE STC GRAPPA},
}
@InProceedings{KollerNiehrenTreinen01,
title = {Dominance Constraints: Algorithms and Complexity},
booktitle = {Third International Conference on Logical Aspects of Computational Linguistics (Dec. 1998, Grenoble, France)},
audience = \{Com1},
author = {Alexander Koller and Joachim Niehren and Ralf Treinen},
year = {2001},
editor = {M. Moortgat},
volume = "2014",
series = LNCS,
publisher = SV,
address = {Heidelberg},
url = {http://www.ps.uni-sb.de/Papers/abstracts/DominanceNP98.html},
abstract = {Dominance constraints for finite tree structures are widely used in
several areas of computational linguistics including syntax,
semantics, and discourse. In this paper, we investigate algorithmic
and complexity questions for dominance constraints and their
first-order theory. We present two NP algorithms for solving dominance
constraints, which have been implemented in the concurrent constraint
programming language Oz. The main result of this paper is that the
satisfiability problem of dominance constraints is NP-complete.
Despite this intractability result, the more sophisticated of our
algorithms performs well in an application to scope
underspecification. We also show that the existential fragment of the
first-order theory of dominance constraints is NP-complete and that
the full first-order theory has non-elementary complexity.},
pages = {106-125},
}
@InProceedings{KuhlmannNiehren08,
author = {Marco Kuhlmann and Joachim Niehren},
title = {Logics and Automata for Totally Ordered Trees},
booktitle = {19th International Conference on Rewriting Techniques and Applications},
audience = \{Com1},
year = 2008,
volume = {5117},
series = LNCS,
month = jul,
publisher = SV,
url = {http://hal.inria.fr/inria-00257278/en},
auteur = {Mostrare STC Grappa ENUM},
abstract = { Totally ordered trees are trees equipped with an additional total order on their nodes. They provide a formal model for data that comes with both a hierarchical and a sequential structure; one example for such data are natural language sentences, where a sequential structure is given by word order, and a hierarchical structure is given by grammatical relations between words. In this paper, we study monadic second"-order logic (MSO) for totally ordered terms. We show that the MSO satisfiability problem of unrestricted structures is undecidable, but give a decision procedure for practically relevant sub"-classes, based on tree automata.
},
pages = {217-231},
}
@InProceedings{KuttlerLhoussaineNiehren07,
booktitle = {Second International Conference on Algebraic Biology},
author = {Céline Kuttler and Cédric Lhoussaine and Joachim Niehren},
title = {A Stochastic Pi Calculus for Concurrent Objects},
audience = \{Com1},
series = LNCS,
publisher = SV,
url = {http://hal.inria.fr/inria-00121104/en},
auteur = {{MOSTRARE STC BIOCOMPUTING GRAPPA HAL:st8orh Hal:41gw6g8d}},
abstract = {We present SpiCO,
a new modeling and simulation language for system biology,
based on the stochastic pi-calculus. SpiCO supports higher
level modeling via multi-profile concurrent objects with static
inheritance. We present a semantics for SpiCO in terms of
continuous time Markov chains, and show how to compile SpiCO
back into the biochemical stochastic pi-calculus while
preserving semantics.
},
volume = {4545},
pages = {232-246},
year = {2007},
month = jul,
}
@InProceedings{LemayManethNiehren10,
author = {Aurélien Lemay and Sebastian Maneth and Joachim Niehren},
booktitle = {29th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems},
audience = \{Com1},
title = {A Learning Algorithm for Top-Down XML Transformations},
url = {http://hal.archives-ouvertes.fr/inria-00460489/en},
abstract = {A generalization from string to trees and
from languages to translations is given of the
classical result that any regular language can be learned
from examples: it is shown that
for any deterministic
top-down tree transformation there exists a sample set of
polynomial size (with respect to the minimal transducer) which allows
to infer the translation.
Until now, only for string transducers and for simple relabeling
tree transducers, similar results had been known.
Learning of deterministic top-down tree transducers (DTOPs)
is far more involved because
a DTOP can copy, delete, and permute its input subtrees.
Thus, complex dependencies of labeled input to output paths
need to be maintained by the algorithm.
First, a Myhill-Nerode theorem is presented for DTOPs,
which is interesting on its own.
This theorem is then used to construct a learning algorithm for
DTOPs. Finally, it is shown how our result can be applied
to XML transformations (e.g. XSLT programs).
For this, a new DTD-based encoding of unranked trees by ranked ones is
presented. Over such encodings, DTOPs can realize
many practically interesting XML transformations
which cannot be realized on
first-child/next-sibling encodings.
},
pages = {285-296},
publisher = ACM,
year = 2010,
auteur = {Mostrare Codex},
}
@InProceedings{LemayNiehrenGilleron06,
author = {Aurélien Lemay and Joachim Niehren and Rémi Gilleron},
title = {Learning n-ary Node Selecting Tree Transducers from Completely Annotated Examples},
booktitle = {{International Colloquium on Grammatical Inference}},
audience = \{Com1},
year = {2006},
volume = {4201},
series = LNAI,
publisher = SV,
url = {http://hal.inria.fr/inria-00088077/en/},
auteur = {MOSTRARE STC GRAPPA RemiGilleron AurelienLemay HAL:xp77#djc},
abstract = {
We present the first algorithm for learning n-ary node selection
queries in trees from completely annotated examples by methods of
grammatical inference. We propose to represent n-ary queries by
deterministic n-ary node selecting tree transducers (NSTTs), that are
known to capture the class of MSO-definable n-ary queries. Despite of
this highly expressive, we show that n-ary queries, selecting a
polynomially bounded number of tuples per tree, represented by
deterministic NSTTs can be learned from polynomial time and data
while allowing for efficient enumeration of query answers. An
application to wrapper induction in Web information extraction yields
encouraging results.
},
pages = {253-267},
}
@InProceedings{LevyNiehrenVillaret05,
author = {Jordi Levy and Joachim Niehren and Mateu Villaret},
title = {Well-nested Context Unification},
booktitle = {20th International Conference on Automated Deduction},
audience = \{Com1},
volume = {3632},
series = LNAI,
month = jun,
publisher = SV,
pages = {149-163},
url = {http://www.ps.uni-sb.de/Papers/abstracts/wellnested-cu.html},
auteur = {MOSTRARE STC GRAPPA},
abstract = {
Context unification (CU) is the famous open problem of
solving context equations for trees. We distinguish
a new decidable fragment of CU - well-nested CU -
and present a new unification algorithm that solves
well-nested context equations in non-deterministic
polynomial time. We show that minimal
well-nested solutions of context equations can be
composed from the material present in the equation.
This surprising property is highly wishful when
modeling natural language ellipsis in CU.
},
year = {2005},
}
@InProceedings{MartensNiehren05,
audience = \{Com1},
booktitle = {10th International Symposium on Database Programming Languages},
author = {Wim Martens and Joachim Niehren},
title = {Minimizing Tree Automata for Unranked Trees},
series = LNCS,
month = aug,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/mini.html},
abstract = {Automata for unranked trees form a foundation for XML schemas,
querying and pattern languages. We study the problem of efficiently
minimizing such automata. We start with the unranked tree automata
(UTAs) that are standard in database theory, assuming bottom-up
determinism and that horizontal recursion is represented by
deterministic finite automata. We show that minimal
UTAs in that class are not unique and that minimization
is NP-hard. We then study more recent automata classes that do allow for
polynomial time minimization. Among those, we show that bottom-up
deterministic stepwise tree automata yield the most succinct
representations.
},
auteur = {MOSTRARE TRALALA STC ACIMDD GRAPPA Query},
pages = {232--246},
year = {2005},
volume = {3774},
}
@InProceedings{MuellerNiehren95,
booktitle = {Asian Computing Science Conference},
author = {Martin Müller and Joachim Niehren},
title = {Constraints for Free in Concurrent Computation},
audience = \{Com1},
address = {Pathumthani, Thailand},
month = dec # { 11--13},
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/ConstraintsFree95.html},
abstract = {We investigate concurrency as unifying computational paradigm which integrates functional, constraint, and object-oriented
programming. We propose the Rho-calculus as a uniform
foundation of concurrent computation and formally relate it
to other models: The Rho-calculus with equational constraints
provides for logic variables and is bisimilar to the
Gamma-calculus. The Rho-calculus without constraints
is a proper subset of the Pi-calculus. We prove its Turing
completeness by embedding the eager Lambda-calculus in
continuation passing style. The Rho-calculus over an
arbitrary constraint system is an extension of the standard
cc-model with procedural abstraction.},
year = {1995},
volume = {1023},
pages = {171--186},
editor = {Kanchanasut, Kanchana and Lévy, Jean-Jacques},
series = LNCS,
}
@InProceedings{MuellerNiehren98,
author = {Martin Müller and Joachim Niehren},
title = {Ordering Constraints over Feature Trees Expressed in Second-order Monadic Logic},
booktitle = {9th International Conference on Rewriting Techniques and Applications},
audience = \{Com1},
year = {1998},
editor = {Tobias Nipkow},
volume = {1379},
series = LNCS,
address = {Tsukuba, Japan},
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/SWSJournal99.html},
abstract = {The system FT$_lt$ of ordering constraints over feature trees has been introduced as an extension of the system FT of equality constraints
over feature trees. We investigate decidability and complexity questions
for fragments of the first-order theory of FT$_lt$. It is well-known that
the first-order theory of FT$_lt$ is decidable and that several of its
fragments can be decided in quasi-linear time, including the
satisfiability problem of FT$_lt$ and its entailment problem
with existential quantification
$$phimodels E x1 ... E xn ( phi' )$$
Much less is known on the first-order theory
of FT$_lt$. The satisfiability problem of FT$_lt$ can be decided in cubic
time, as well as its entailment problem without existential
quantification. Our main result is that the entailment
problem of FT$_lt$ with existential quantifiers is
decidable but PSPACE-hard. Our decidability proof is based on a
new technique where feature constraints are expressed in second-order
monadic logic with countably many successors SwS. We thereby reduce
the entailment problem of FT$_lt$ with existential quantification
to Rabin's famous theorem on tree automata.},
pages = {196--210},
}
@InProceedings{MuellerNiehrenPodelski97a,
author = {Martin Müller and Joachim Niehren and Andreas Podelski},
title = {Ordering Constraints over Feature Trees},
booktitle = {3rd International Conference on Principles and Practice of Constraint Programming},
audience = \{Com1},
year = {1997},
editor = {Gert Smolka},
volume = {1330},
series = LNCS,
address = {Schloss Hagenberg, Linz, Austria},
month = "29 "#oct#"--1 "#nov,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/ftsub-constraints-99.html},
abstract = {Feature trees have been used to accommodate records in constraint programming and record like structures in computational linguistics.
Feature trees model records, and feature constraints
yield extensible and modular record descriptions. We introduce the
constraint system FT$<$ of ordering constraints interpreted over
feature trees. Under the view that feature trees represent symbolic
information, the relation $<$ corresponds to the information
ordering (carries less information than). We present a
polynomial
algorithm that decides the satisfiability of conjunctions of positive
and negative information ordering constraints over feature trees. Our
results include algorithms for the satisfiability problem and the
entailment problem of FT$<$ in time $O(n^3)$. We also
show that
FT$<$ has the independence property and are thus able to handle
negative conjuncts via entailment. Furthermore, we reduce the
satisfiability problem of D{"o}rre's weak-subsumption constraints to
the satisfiability problem of FT$<$. This improves the complexity
bound for solving weak subsumption constraints from
$O(n^5)$ to $O(n^3)$.},
pages = {297--311},
}
@InProceedings{MuellerNiehrenPodelski97b,
title = {Inclusion Constraints over Non-Empty Sets of Trees},
booktitle = {Theory and Practice of Software Development, International Joint Conference CAAP/FASE/TOOLS},
audience = \{Com1},
author = {Martin Müller and Joachim Niehren and Andreas Podelski},
publisher = SV,
pages = {217-231},
url = {http://www.ps.uni-sb.de/Papers/abstracts/ines97.html},
abstract = {We present a new constraint system called Ines. Its constraints are
conjunctions of inclusions $t_1subseteq t_2$
between first-order terms
(without set operators) which are interpreted over non-empty sets of
trees. The existing systems of set constraints can express Ines
constraints only if they include negation. Their satisfiability
problem is NEXPTIME-complete. We present an incremental
algorithm that solves the satisfiability problem of Ines
constraints in cubic time. We intend to apply Ines constraints for
type analysis for a concurrent constraint programming language.},
editor = {Max Dauchet},
year = {1997},
volume = {1214},
series = LNCS,
month = apr,
}
@InProceedings{MuellerNiehrenTalbot99,
author = {Martin Müller and Joachim Niehren and Jean-Marc Talbot},
title = {Entailment of Atomic Set Constraints is {PSPACE}-Complete},
booktitle = {Fourteenth Annual IEEE Symposium on Logic in Computer Sience},
audience = \{Com1},
year = {1999},
address = { Trento, Italy},
month = jul,
note = {An extended version is available at url{www.ps.uni-sb.de/Papers/abstracts/atomic:98.html}},
publisher = IEEECSP,
url = {http://www.ps.uni-sb.de/Papers/abstracts/atomic-lics-99.html},
abstract = {The complexity of set constraints has been extensively studied over the last years and was often found quite high. At the lower end of
expressiveness, there are atomic set constraints which are
conjunctions of inclusions t1 $subseteq$ t2
between first-order terms
without set operators. It is well-known that satisfiability of atomic
set constraints can be tested in cubic time. Also, entailment of
atomic set constraints has been claimed decidable in polynomial
time. We refute this claim. We show that entailment between atomic set
constraints can express validity of quantified boolean
formulas and is thus PSPACE hard. For infinite signatures, we also
present a PSPACE-algorithm for solving atomic set constraints with
negation. This proves that entailment of atomic set constraints is
PSPACE-complete for infinite signatures. In case of finite
signatures, this problem is even DEXPTIME-hard.},
pages = {285--294},
}
@InProceedings{MuellerNiehrenTreinen98,
audience = \{Com1},
author = {Martin Müller and Joachim Niehren and Ralf Treinen},
title = {The First-Order Theory of Ordering Constraints over Feature Trees},
booktitle = {13th annual IEEE Symposium on Logic in Computer Sience},
year = {1998},
abstract = {The system FT${}_leq$ of ordering constraints over feature trees has been introduced as an
extension of the system FT of equality constraints over feature
trees. We investigate the first-order theory of FT${}_leq$
and its fragments in detail, both
over finite trees and over possibly infinite trees. We prove that the
first-order theory of FT${}_leq$
is undecidable, in contrast to the first-order theory of FT
which is well-known to be decidable. We show that the entailment
problem of FT${}_leq$ with
existential quantification is PSPACE-complete. So far, this problem
has been shown decidable, coNP-hard in case of finite trees,
PSPACE-hard in case of arbitrary trees, and cubic time when restricted
to quantifier-free entailment judgments. To show PSPACE-completeness,
we show that the entailment problem of FT${}_leq$ with existential
quantification is equivalent to the
inclusion problem of non-deterministic finite automata.},
address = {Indianapolis, Indiana},
pages = {432--443},
month = {21--24 June},
publisher = IEEECSP,
url = {http://www.ps.uni-sb.de/Papers/abstracts/FTSubTheory-Long:99.html},
}
@InProceedings{Niehren96,
title = {Functional Computation as Concurrent Computation},
booktitle = {$23^{th}$ Proceedings of the {ACM} Symposium on Principles of Programming Languages},
author = {Joachim Niehren},
audience = \{Com1},
note = {longer version appeared as DFKI Research Report RR-95-14},
year = {1996},
abstract = {We investigate functional computation as a special form of concurrent computation. As formal basis, we use a
uniformly confluent core of the pi-calculus,
which is
also contained in models of higher-order concurrent
constraint programming. We embed the call-by-need
and the call-by-value lambda-calculus
into the
pi-calculus. We prove that call-by-need
complexity is
dominated by call-by-value complexity. In contrast to
the recently proposed call-by-need lambda-calculus,
our concurrent call-by-need model incorporats mutual
recursion and can be extended to cyclic data structures
by means of constraints.},
url = {http://www.ps.uni-sb.de/Papers/abstracts/POPL96.html},
pages = {333--343},
month = {21--24}#jan,
publisher = ACM,
}
@InProceedings{NiehrenKoller01,
booktitle = {Proceedings of the 3rd International Conference on Logical Aspects of Computational Linguistics (Dec. 1998, Grenoble, France)},
author = {Joachim Niehren and Alexander Koller},
title = {Dominance Constraints in Context Unification},
audience = \{Com1},
year = {2001},
editor = {M. Moortgat},
volume = "2014",
series = LNCS,
address = {Heidelberg},
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/Dominance-98.html},
abstract = {Tree descriptions based on dominance constraints are popular in several areas of computational linguistics including syntax,
semantics, and discourse. Tree descriptions in the language of context
unification have attracted some interest in unification and rewriting
theory. Recently, dominance constraints and context unification
have both been used in different underspecified approaches to the semantics
of scope, parallelism, and their interaction. This raises the
question whether both description languages are related. In this
paper, we show for a first time that dominance constraints can be
expressed in context unification. We
also prove that dominance constraints extended with parallelism
constraints are equal in expressive power to context unification.},
key = {c6},
pages = {199-218},
}
@InProceedings{NiehrenPinkalRuhrberg97,
title = {A Uniform Approach to Underspecification and Parallelism},
booktitle = {35th Annual Meeting of the Association of Computational Linguistics},
audience = \{Com1},
author = {Joachim Niehren and Manfred Pinkal and Peter Ruhrberg},
address = {Madrid, Spain},
month = "7--11"#jul,
url = {http://www.ps.uni-sb.de/Papers/abstracts/Ellipses.html},
abstract = {We propose a unified framework in which to treat semantic underspecification and
parallelism phenomena in discourse. The
framework employs a constraint language
that can express equality and subtree
relations between finite trees. In addition,
our constraint language can express the
equality up-to relation over trees which
captures parallelism between them. The
constraints are solved by context
unification. We demonstrate the use of
our framework at the examples of quantifier
scope, ellipses, and their interaction.},
pages = {410-417},
year = {1997},
}
@InProceedings{NiehrenPinkalRuhrberg97a,
author = {Joachim Niehren and Manfred Pinkal and Peter Ruhrberg},
title = {On Equality Up-to Constraints over Finite Trees, Context Unification and One-Step Rewriting},
booktitle = {Proceedings of the International Conference on Automated Deduction},
audience = \{Com1},
pages = {34-48},
year = {1997},
volume = {1249},
series = LNCS,
address = {Townsville, Australia},
publisher = SV,
month = "14-17"#jul,
url = {http://www.ps.uni-sb.de/Papers/abstracts/fullContext.html},
abstract = {We introduce equality up-to constraints over finite trees and investigate their expressiveness. Equality up-to
constraints subsume equality constraints, subtree constraints,
and one-step rewriting constraints.
We establish a close correspondence between
equality up-to constraints over finite trees and context unification.
Context unification subsumes string unification and is subsumed by
linear second-order unification. We obtain the following
three new results.
The satisfiability problem of equality up-to constraints is
equivalent to context unification, which is an open problem.
The positive existential fragment of the theory of one-step
rewriting is decidable. The E*A*E*
fragment of the theory of context unification is undecidable.},
}
@InProceedings{NiehrenPlanqueTalbotTison05,
author = {Joachim Niehren and Laurent Planque and Jean-Marc Talbot and Sophie Tison},
booktitle = {10th International Symposium on Database Programming Languages},
title = {N-ary Queries by Tree Automata} ,
audience = \{Com1},
pages = {217--231},
publisher = SV,
annote = {An earlier version has been presented at the 19th International Workshop on Unification},
url = {http://www.ps.uni-sb.de/Papers/paper_info.php?label=n-ary-query},
auteur = {MOSTRARE TRALALA STC GRAPPA ACIMDD},
abstract = {We investigate n-ary node selection queries in trees
by successful runs of tree automata. We show
that run-based n-ary queries capture MSO, contribute
algorithms for enumerating answers of n-ary queries,
and study the complexity of the problem. We investigate
the subclass of run-based n-ary queries by unambiguous
tree automata.
Keywords: XML databases, logic, automata.
} ,
month = sep,
year = 2005,
volume = {3774},
series = LNCS,
}
@InProceedings{NiehrenPodelski93,
title = {Feature Automata and Recognizable Sets of Feature Trees},
booktitle = {TAPSOFT: Theory and Practice of Software Development: Joint International Conference CAAP/FASE/TOOLS.},
audience = \{Com1},
author = {Joachim Niehren and Andreas Podelski},
editor = {Marie-Claude Gaudel and Jean-Pierre Jouannaud},
volume = {668},
series = LNCS,
url = {http://www.ps.uni-sb.de/Papers/abstracts/CAAP1993.html},
publisher = SV,
abstract = {Feature trees generalize first-order trees whereby argument positions become keywords (features) from an infinite symbol set . Constructor symbols can occur with any argument positions, in any finite number. Feature trees are used to model flexible records; the assumption on the infiniteness of accounts for dynamic record field updates.
We develop a universal algebra framework for feature trees. We introduce the classical set-defining notions: automata, regular expressions and equational systems, and show that they coincide. This extension of the regular theory of trees requires new notions and proofs. Roughly, a feature automaton reads a feature tree in two directions: along its branches and along the fan-out of each node.
We illustrate the practical motivation of our regular theory of feature trees by pointing out an application on the programming language LIFE.
},
pages = {356--375},
year = {1993},
}
@InProceedings{NiehrenPodelskiTreinen93,
author = {Joachim Niehren and Andreas Podelski and Ralf Treinen},
title = {Equational and Membership Constraints for Infinite Trees},
booktitle = {Proceedings. Fifth International Conference on Rewriting Techniques and Applications},
audience = \{Com1},
year = 1993,
editor = {Claude Kirchner},
volume = {690},
series = LNCS,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/RR-93-14.html},
abstract = {We present a new constraint system with equational and membership
constraints over infinite trees. It provides for complete and correct
satisfiability and entailment tests and is therefore suitable for the
use in concurrent constraint programming systems which are based on
cyclic data structures.Our set defining devices are greatest
fixpoint solutions of iregular systems of equations with a
deterministic form of union. As the main technical particularity of
the algorithms we present a novel memorization technique. We believe
that both satisfiability and entailment tests can be implemented in an
efficient and incremental manner.},
pages = {106-120},
}
@InProceedings{NiehrenPriesnitz01,
author = {Joachim Niehren and Tim Priesnitz},
title = {Non-Structural Subtype Entailment in Automata Theory},
booktitle = {Fourth International Symposium on Theoretical Aspects of Computer Software
(TACS2001)},
audience = \{Com1},
year = {2001},
address = {Sendai, Japan},
month = oct#{ 28-31},
url = {http://www.ps.uni-sb.de/Papers/abstracts/pauto.html},
abstract = {Decidability of non-structural subtype entailment is a long standing open problem in programming language
theory. In this paper, we apply automata theoretic
methods to characterize the problem equivalently
by using regular expressions and word equations.
This characterization induces new results on
non-structural subtype entailment, constitutes
a promising starting point for further investigations
on decidability, and explains for the first time
why the problem is so difficult. The difficulty
is caused by implicit word equations that we make
explicit.},
pages = {360--384},
}
@InProceedings{NiehrenPriesnitz99,
booktitle = {Asian Computing Science Conference},
audience = \{Com1},
author = {Joachim Niehren and Tim Priesnitz},
title = {Entailment of Non-Structural Subtype Constraints},
year = {1999},
editor = {P. S. Thiagarajan and Roland H. C. Yap},
volume = {1742},
series = LNCS,
address = {Phuket, Thailand},
publisher = SV,
month = dec#{ 10-12},
url = {http://www.ps.uni-sb.de/Papers/abstracts/SubTypeEntailment:99.html},
abstract = {Entailment of subtype constraints was introduced for constraint simplification in subtype inference systems.
Designing an efficient algorithm for subtype entailment
turned out to be surprisingly difficult. The situation was
clarified by Rehof and Henglein who proved entailment
of structural subtype constraints to be coNP-complete for
simple types and PSPACE-complete for recursive types. For
entailment of non-structural subtype constraints of both
simple and recursive types they proved PSPACE-hardness
and conjectured PSPACE-completeness
but failed in finding a complete algorithm. In this paper,
we investigate the source of complications and isolate a
natural subproblem of non-structural subtype entailment
that we prove PSPACE-complete. We conjecture (but this
is left open) that the presented approach can be
extended to the general case.},
pages = {251--265},
}
@InProceedings{NiehrenPriesnitzSu05,
author = {Joachim Niehren and Tim Priesnitz and Zhendong Su},
title = {Complexity of Subtype Satisfiability over Posets},
booktitle = {14th European Symposium on Programming},
audience = \{Com1},
year = 2005,
volume = {3444},
series = LNCS,
month = apr,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/pdl05.html},
auteur = {JoachimNiehren MOSTRARE STC GRAPPA},
abstract = {Subtype satisfiability is an important problem for designing advanced
subtype systems and subtype-based program analysis algorithms. The
problem is well understood if the atomic types form a lattice. However,
little is known about subtype satisfiability over posets. In this
paper, we investigate algorithms for and the complexity of subtype
satisfiability over general posets. We present a uniform treatment of
different flavors of subtyping: simple versus recursive types and
structural versus non-structural subtype orders. Our results are
established through a new connection of subtype constraints and modal
logic. As a consequence, we settle a problem left open by Tiuryn and
Wand in 1993.},
pages = {357-373},
}
@InProceedings{NiehrenSabelSchmidt-Schauss07,
author = {Joachim Niehren and David Sabel and Manfred Schmidt-Schauß and Jan Schwinghammer},
title = {Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures},
booktitle = {23rd Conference on Mathematical Foundations of Programming Semantics},
audience = \{Com1},
year = {2007},
volume = 173,
series = ENTCS,
month = apr,
publisher = ELSEVIER,
url = {http://hal.inria.fr/inria-00128861/en},
auteur = {MOSTRARE GRAPPA STC TRALALA HAL:4bw8tta},
abstract = {
We present an observational semantics for lambda(fut), a
concurrent lambda calculus with reference cells and
futures. The calculus lambda(fut) models the operational
semantics of the concurrent higher-order programming language
Alice ML. Our result is a powerful notion of equivalence
that is the coarsest nontrivial congruence distinguishing
observably different processes. It justifies a maximal set
of correct program transformations, and it includes all of
lambda(fut)'s deterministic reduction rules, in particular,
call-by-value beta reduction.
},
pages = {313-337},
}
@InProceedings{NiehrenSmolka94,
author = {Joachim Niehren and Gert Smolka},
title = {A Confluent Relational Calculus for Higher-Order Programming with Constraints},
booktitle = {1st International Conference on Constraints in Computational Logics},
audience = \{Com1},
editor = "Jean-Pierre Jouannaud",
volume = {845},
series = LNCS,
month = "7--9 " # sep,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/RhoCCL94.html},
abstract = {We present the rho-calculus, a relational calculus
parametrized by a logical constraint system. The rho-calculus provides
for higher-order relational programming with first-order constraints,
and subsumes higher-order functional programming as a special case.
It captures important aspects of the concurrent constraint programming language Oz.
We prove the uniform confluence of the rho-calculus.
Uniform confluence implies that all maximal derivations
issuing from a given expression have equal length.
But even confluence of a nonfunctional calculus modelling
computation with partial information is interesting
on its own right.},
year = {1994},
}
@InProceedings{NiehrenThater03,
audience = \{Com1},
author = {Joachim Niehren and Stefan Thater},
title = {Bridging the Gap Between Underspecification Formalisms: Minimal Recursion Semantics as Dominance Constraints},
booktitle = {{41st Meeting of the Association of Computational Linguistics}},
month = jul,
auteur = {MOSTRARE GRAPPA STC},
url = {http://www.ps.uni-sb.de/Papers/abstracts/mrs_dom.html},
abstract = {Minimal Recursion Semantics (MRS) is the standard formalism used in large-scale HPSG grammars to model underspecified semantics. We
present the first provably efficient algorithm to enumerate the
readings of MRS structures. It is obtained by translating MRS
into normal dominance constraints for which efficient
algorithms exist.},
pages = {367-374},
year = {2003},
}
@InProceedings{NiehrenVillaret02,
author = {Joachim Niehren and Mateu Villaret},
title = {Parallelism and Tree Regular Constraints},
booktitle = {International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
audience = \{Com1},
year = "2002",
volume = "2514",
series = LNAI,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/sdom.html},
pages = {311--326},
}
@InProceedings{NiehrenVillaret05,
booktitle = {5th International Conference on Logical Aspects in Computational Linguistics} ,
author = {Joachim Niehren and Mateu Villaret},
title = {Describing Lambda Terms in Context Unification},
audience = \{Com1},
month = apr,
publisher = SV,
url = {http://www.ps.uni-sb.de/Papers/abstracts/clls-cu.html},
auteur = {JoachimNiehren MOSTRARE STC GRAPPA},
abstract = {The constraint language for lambda structures (CLLS) is
a description language for lambda terms. CLLS provides
parallelism constraints to talk about the tree structure
of lambda terms, and lambda binding constraints to specify
variable binding.
Parallelism constraints alone have
the same expressiveness as context unification. In this paper,
we show that lambda binding constraints can also be expressed
in context unification when permitting tree
regular constraints. },
series = LNAI,
pages = {221-237},
year = 2005,
volume = {3492},
}
@InProceedings{Schmidt-SchaussNiehrenSabel08,
author = {Manfred Schmidt-Schauß and Joachim Niehren and David Sabel and Jan Schwinghammer},
title = {Adequacy of Compositional Translations for Observational Semantics},
booktitle = {5th IFIP International Conference on Theoretical Computer Science},
audience = \{Com1},
year = 2008,
volume = {273},
publisher = SV,
url = {http://hal.inria.fr/inria-00257279/en},
auteur = {{Mostrare STC Grappa concurrent programming}},
abstract = {We investigate methods and tools for analysing translations
between programming languages with respect to
observational semantics. The behaviour of programs is
observed in terms of may- and must-convergence in arbitrary
contexts, and adequacy of translations, i.e., the reflection
of program equivalence, is taken to be the fundamental
correctness condition.
For compositional translations we propose a notion of
convergence equivalence as a means
for proving adequacy.
This technique avoids explicit reasoning about
contexts, and is able to deal with the subtle role of typing in
implementations of language extension.
},
pages = {521-535},
}
@InProceedings{StaworkoLaurenceLemay09,
title = {Equivalence of Nested Word to Word Transducers},
booktitle = {17th International Symposium on Fundamentals of Computer Theory},
author = {Slawek Staworko and Grégoire Laurence and Aurélien Lemay and Joachim Niehren},
audience = \{Com1},
volume = {5699},
series = LNCS,
abstract = {We study the equivalence problem of deterministic nested word to word transducers and show it to be surprisingly robust. Modulo polynomial time reductions, it can be identified with 4 equivalence problems for diverse classes of deterministic non-copying order-preserving transducers. In particular, we present polynomial time back and fourth reductions to the morphism equivalence problem on context free languages, which is known to be solvable in polynomial time.},
auteur = {Mostrare Codex},
pages = {310-322},
publisher = SV,
year = 2009,
url = {http://hal.archives-ouvertes.fr/hal-00399804/en},
}
@InProceedings{ZhendongAikenNiehrenPriesnitzTreinen02,
booktitle = {The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
author = {Zhendong Su and Alexander Aiken and Joachim Niehren and Tim Priesnitz and Ralf Treinen},
title = {First-Order Theory of Subtyping Constraints},
audience = \{Com1},
publisher = ACM,
url = {http://www.ps.uni-sb.de/Papers/abstracts/fot02.html},
address = {Portland, USA},
year = {2002},
abstract = {We investigate the first-order theory of subtyping constraints. We show that the first-order theory of non-structural subtyping is undecidable,
and we show that in the case where all constructors are either unary or
nullary, the first-order theory is decidable for both structural and
non-structural subtyping. The decidability results are shown by
reduction to a decision problem on tree automata. This work is a step
towards resolving long-standing open problems of the decidability of
entailment for non-structural subtyping.},
month = jan,
}
@InProceedings{CarmeGilleronLemayNiehren05,
author = {Julien Carme and Rémi Gilleron and Aurélien Lemay and Joachim Niehren},
title = {Interactive Learning of Node Selecting Tree Transducer},
booktitle = {{IJCAI Workshop on Grammatical Inference}},
audience = \{Pos1},
annote = {Extended version published at Machine Learning \cite{CarmeGilleronLemayNiehren07}.},
url = {http://hal.ccsd.cnrs.fr/view_by_stamp.php?label=INRIA&langue=en&action_todo=view&id=inria-00087226&version=2},
auteur = {RemiGilleron AurelienLemay JulienCarme },
abstract = {
We present a new learning process for Web information
extraction, that is visually interactive. Web documents are
considered as trees in which wrappers select sets of nodes.
We start from a recent algorithm that induces node selection
queries in trees by
methods of grammatical inference. We then show how to turn this
algorithm into our visually interactive learning process, using
intelligent tree pruning heuristics. Experiments on realistic Web
documents confirm excellent quality with very few user
interactions -- annotations and corrections -- during wrapper induction.
},
year = {2005},
}
@InProceedings{ChampavereGilleronLemay07,
author = {Jérôme Champavère and Rémi Gilleron and Aurélien Lemay and Joachim Niehren},
title = {Towards Schema-Guided {XML} Query Induction},
booktitle = {ICML-2007 Workshop on Challenges and Applications of Grammar Induction},
audience = \{Pos1},
url = { http://www.grappa.univ-lille3.fr/~champavere/Recherche/publications/cagi07_paper.pdf },
auteur = {MOSTRARE STC QUERY GRAPPA},
abstract = {The induction of node selection queries in XML documents
is a key task in Web information
extraction. Recent approaches based on grammatical
inference represent node selection queries by deterministic
tree automata. In this paper, we show
how to guide RPNI-based learning algorithms by XML schemas
which we can infer in a preprocessing step.
We hope that schema guidance will help to improve
heuristics that are essential for query learning algorithms.
},
year = {2007},
}
@InProceedings{FiliotNiehrenTalbotTison06,
title = "Composing Monadic Queries in Trees",
booktitle = "PLAN-X International Workshop",
audience = \{Pos1},
author = "Emmanuel Filiot and Joachim Niehren and Jean-Marc Talbot and Sophie Tison",
abstract = {Node selection in trees is a fundamental operation to XML databases, programming languages, and information extraction. We propose a new class of querying languages to define n-ary queries. The choice of the underlying monadic querying language is parametric. We show that compositions of monadic MSO-definable queries capture n-ary MSO-definable queries, and distinguish an MSO-complete n-ary query language that enjoys an efficient query answering algorithm.},
pages = {61--70},
publisher = BRICS,
year = "2006",
editor = "Giuseppe Castagna and Mukund Raghavachari",
url = {http://www2.lifl.fr/~filiot/Plan-X-final-version.pdf},
auteur = {MOSTRARE STC TRALALA GRAPPA Query},
}
@InProceedings{GauwinCaronNiehren08,
author = {Olivier Gauwin and Anne-Cécile Caron and Joachim Niehren and Sophie Tison},
title = {Complexity of Earliest Query Answering with Streaming Tree Automata},
booktitle = {ACM SIGPLAN Workshop on Programming Language Techniques for XML (PLAN-X)},
audience = \{Pos1},
month = jan,
note = {PLAN-X Workshop of ACM POPL},
url = {http://hal.inria.fr/inria-00336169},
auteur = {{MOSTRARE STC Tralala GRAPPA ENUM}},
abstract = {We investigate the complexity of earliest query answering
for n-ary node selection queries defined by streaming
tree automata (STAs). We elaborate an algorithm that selects
query answers upon reception of the shortest relevant prefix of
the input tree on the stream. For queries defined by
deterministic STAs, our algorithm runs in polynomial time
combined complexity. In the general case, we show that earliest
query answering is DEXPTIME-hard (even for n=0)
and thus DEXPTIME-complete. },
year = {2008},
}
@InProceedings{KuttlerLhoussaineNiehren06,
booktitle = {1st International Workshop on Probabilistic Automata and Logics},
audience = \{Pos1},
author = {Céline Kuttler and Cédric Lhoussaine and Joachim Niehren},
title = {A Stochastic Pi Calculus for Concurrent Objects},
auteur = {MOSTRARE STC BIOCOMPUTING GRAPPA HAL:st8orh},
year = {2006},
url = {http://hal.inria.fr/inria-00121104/en},
abstract = {We present SpiCO,
a new modeling and simulation language for system biology,
based on the stochastic pi-calculus. SpiCO supports higher
level modeling via multi-profile concurrent objects with static
inheritance. We present a semantics for SpiCO in terms of
continuous time Markov chains, and show how to compile SpiCO
back into the biochemical stochastic pi-calculus while
preserving semantics.
},
}
@InProceedings{NiehrenSchwinghammerSmolka05,
author = {Joachim Niehren and Jan Schwinghammer and Gert Smolka},
title = {A Concurrent Lambda Calculus with Futures},
booktitle = {5th International Workshop on Frontiers in Combining Systems},
audience = \{Pos1},
volume = {3717},
year = {2005},
url = {http://hal.ccsd.cnrs.fr/view_by_stamp.php?label=INRIA&langue=fr&action_todo=view&id=inria-00090434&version=2},
auteur = {MOSTRARE GRAPPA STC},
abstract = {
We introduce a new concurrent lambda calculus with futures,
lambda(fut), to model the operational semantics of Alice, a
concurrent extension of ML. lambda(fut) is a minimalist
extension of the call-by-value lambda-calculus that yields
the full expressiveness to define, combine, and implement
a variety of standard concurrency constructs such as channels,
semaphores, and ports. We present a linear type system for
lambda(fut) by which the safety of such definitions
and their combinations can be proved:
Well-typed implementations cannot be corrupted in any well-typed context.
},
pages = {248-263},
month = aug,
publisher = SV,
series = LNAI,
}
@InProceedings{SchwinghammerSabelSchmidt-Schauss09,
booktitle = {Workshop on ML},
author = {Jan Schwinghammer and David Sabel and Manfred Schmidt-Schauss and Joachim Niehren},
audience = \{Pos1},
title = {Correctly Translating Concurrency Primitives},
abstract = { Motivated by the question of correctness of a specific implementation of
concurrent buffers in the lambda calculus with futures underlying Alice ML,
we prove that concurrent buffers and
handled futures can correctly encode each other. Our translations
map waiting on handled futures to queuing of concurrent buffers
and vice versa.
Correctness of translations means that they preserve and reflect the
observations of may- and must-convergence.
As a consequence of
compositionality, they are also adequate with respect to a
contextually defined notion of observational program semantics.
We demonstrate that our approach to the correctness of implementations applies uniformly to the whole
compilation process from high-level to
low-level concurrent languages.},
year = 2009,
auteur = {Mostrare},
month = may,
publisher = ACM,
pages = {27-38},
url = {http://www.grappa.univ-lille3.fr/~niehren/Papers/buffer/0.pdf},
}
%========================== Book ==========================
@Book{DuchierGardentNiehren98,
year = {1998},
title = {Concurrent Constraint Programming in Oz for Natural Language Processing},
audience = \{OUVR},
author = {Denys Duchier and Claire Gardent and Joachim Niehren},
abstract = {
},
address = {Universit{"a}t des Saarlandes, Germany},
note = {On-line lecture notes available at url{http://www.ps.uni-sb.de/Papers}},
url = {http://www.ps.uni-sb.de/Papers/abstracts/Oz_NLP.html},
}
%========================== InCollection ==========================
@InCollection{KollerNiehren02,
author = {Alexander Koller and Joachim Niehren},
title = {Constraint Programming in Computational Linguistics},
booktitle = {Words, Proofs, and Dialog},
audience = \{OUVR},
pages = {95-122},
year = {2002},
editor = {Dave Barker-Plummer and David I. Beaver and Johan van Benthem and Patrick Scotto di Luzio},
volume = "141",
url = {http://www.ps.uni-sb.de/Papers/abstracts/CP-NL.html},
abstract = {Constraint programming is a programming paradigm that was originally invented in computer science to deal with hard
combinatorial problems. Recently, constraint programming has
evolved into a technology which permits to solve hard industrial
scheduling and optimization problems. We argue
that existing constraint programming technology can be useful for
applications in natural language processing. Some problems whose
treatment with traditional methods requires great care to avoid
combinatorial explosion of (potential) readings seem to be solvable in
an efficient and elegant manner using constraint programming. We
illustrate our claim by two recent examples, one from the area of
underspecified semantics and one from parsing.},
key = "w1",
}
%========================== Misc ==========================
@Misc{KollerNiehren99,
audience = \{OUVR},
title = {Scope Underspecification and Processing},
howpublished = {Reader for the ESSLLI summer school.},
month = {last Revision: }#jul#{ 21},
year = {1999},
abstract = {This reader contains material for the ESSLLI '99 course, ``Scope Underspecification and Processing''. The reader and course are
aimed at a pretty broad audience; we have tried to only presuppose
a very general idea of natural language processing and of
first-order logic.
Underspecification is a general approach to dealing with
ambiguity. In the course, we'll be particularly concerned with
scope underspecification, which deals with scope ambiguity, a
structural ambiguity of the semantics of a sentence. As scope
underspecification is at least partially motivated by computational
issues, we will pay particular attention to processing aspects.
We're going to show how dominance constraints can be used for
scope underspecification and how they can be processed
efficiently by using concurrent constraint programming
technology.},
author = {Alexander Koller and Joachim Niehren},
url = {http://www.ps.uni-sb.de/Papers/abstracts/ESSLLI:99.html},
}
%========================== PhdThesis ==========================
@PhdThesis{Niehren94,
school = {Universität des Saarlandes, Fachbereich Informatik},
audience = \{phd},
year = {1994},
author = {Joachim Niehren},
title = {Funktionale Berechnung in einem uniform
nebenläufigen Kalkül mit logischen Variablen},
abstract = {Doctoral Dissertation, December 1994, Universität des Saarlandes.
In German. In English: functional computation in a uniformly concurrent
calculus with logic variables.
We present the delta-calculus, a model
of uniformly concurrent computation. It integrates eager and lazy functional
computation and describes the intended complexity behavior
in both cases.
We call concurrent computation uniformly concurrent, if result,
termination and complexity are independent from the computation
order. We establish theses properties for the delta-calculus by
proving its uniform confluence.
The delta-calculus extends to models of concurrent computation
providing for consumable resources and indeterminism. Such are the
gamma-calculus, a foundation of concurrent computation with constraints,
and the pi-calculus, a successor of CCS based on channel communication.
The delta-calculus is a relational calculus with procedural abstraction
and application. It provides for communication over logic variables and
for suspension on their instantiation. Both mechanisms come naturally with
parallel composition and declaration.
We embed the eager and the lazy lambda-calculus into the delta-calculus.
Using explicit references we guarantee that functional arguments are evaluated
at most once. Explicit references are a special form of logic variables. These
are needed too for representing lazy functional control. We prove the adequacy
of the embedding of the eager lambda-calculus with respect to termination and
complexity. We conjecture that the embedding of the lazy lambda-calculus
preserves termination and improves complexity.},
address = {Saarbr{"u}cken, Germany},
month = dec,
url = {http://www.ps.uni-sb.de/Papers/abstracts/PhD-Niehren.html},
}
%========================== Article ==========================
@Article{ChampavereGilleronetAl10,
author = "Jérome Champavère and Rémi Gilleron and Aurélien Lemay and Joachim Niehren",
year = 2010,
audience = \{AUTRES},
title = "Schema-Guided Query Induction",
journal = JMLR,
annote = "en cours de soumission",
auteur = {CODEX AurelienLemay JeromeChampavere JoachimNiehren RemiGilleron MOSTRARE},
url = {javascript:void(0);},
}
%========================== InProceedings ==========================
@InProceedings{GauwinNiehren10,
author = {Olivier Gauwin and Joachim Niehren},
title = {Streamable Fragments of {Forward XPath}},
audience = \{AUTRES},
url = {http://www.grappa.univ-lille3.fr/~niehren/Papers/streamability/0.pdf},
abstract = {Numerous algorithms were proposed for answering XPath
queries on XML streams, but no satisfactory classification
into streamable and non-streamable XPath fragments exists. The large
gap between current upper and lower bounds is raised by the usage of
too general machine models in proofs of lower bounds.
In this paper, we provide the first
satisfactory classification into streamable and non-streamable
fragments of Forward XPath. Our classification
is based
on a new notion of streamability, that we call finite
streamability,
which applies to languages of monadic
queries on unranked trees.
Finite streamability restricts both space and time polynomially,
while assuming a realistic machine model satisfied by all existing
streaming algorithms in the literature. In particular, we assume that
alive answer candidates are buffered in registers without compaction
tricks. Our first technical contribution is a proof, that a query
language cannot be finitely streamable, if its satisfiability problem is
not tractable. This result implies the non-streamability of even
thin fragments of Forward XPath, while contradicting positive
streamability results in the literature. Our second technical result
is a new algorithm showing finite streamability for
k-Downward XPath, a fragment of Forward XPath on documents
with restricted recursion, where the branching depth of
path expressions is bounded by k. Our algorithm is obtained
by P-timeE compilation of k-Downward XPath expressions to deterministic
nested word automata, for which finite streamability
was established recently.
Keywords: XML, streams, queries, schemas, logic, automata.},
year = 2010,
auteur = {Mostrare Codex ENUM},
}
%========================== Article ==========================
@Article{SuAikenNiehrenPriesnitzTreinen05,
journal = TOPLAS,
year = 2006,
audience = \{AUTRES},
author = {Zhendong Su and Alexander Aiken and Joachim Niehren and Tim Priesnitz and Ralf Treinen},
title = {First-Order Theory of Subtyping Constraints},
url = {http://www.ps.uni-sb.de/Papers/abstracts/sub-journal.html},
abstract = {We investigate the first-order theory of subtyping constraints. We show that the first-order theory of non-structural subtyping is undecidable, and we show that in the case where all constructors are either unary or nullary, the first-order theory is decidable for both structural and non-structural subtyping.
Our results hold for both simple and recursive types. The undecidability result is shown by a reduction from the Post's Correspondence Problem, and
the decidability results are shown by a reduction to a decision problem on tree automata. In addition, we introduce the notion of a constrained tree automaton to express non-structural subtype entailment.
This work is a step towards resolving long-standing open problems of the decidability of entailment for non-structural subtyping.},
note = {Extended Version of ACM POPL 2002},
auteur = {MOSTRARE STC GRAPPA},
}
