For a full list of papers, see my CV
(PDF).
Mona
The papers below are just a sample. Please see papers
at the Mona web site for a full list.
Automata theory
-
Relativizations for
the logic-automaton connection. (Submitted.) The
mathematical framework Mona uses for handling first-order
variables and relativizations. This paper introduces
ternary and sexpartite valuations to capture relativized
formulas under an automata-theoretic view.
-
An n log n algorithm for
online BDD refinement. (J. of Alg., 1999.) A
minimization construction for BDD-represented
automata. The path compression of BDDs makes Hopcroft's
algorithm unworkable, but some rather involved
techniques make an n log n algorithm possible.
Verification
Programming languages
& XML
-
XML:
Model, Schemas, Types, Logics and Queries (Draft
version, with Thomas Schwentick and Dan Suciu, final
version to appear in Logics of emerging applications
of databases, Eds. J. Chomicki, G. Saake, and R. van
der Meyden, Springer Verlag, 2003.) We introduce XML,
provide a mathematical model, explain DOM, XPath and XSLT,
discuss schema and tree languages, work out the relevance
of tree automata and monadic-second-order logic to XML,
present decidability results for typing of XML, and
survey related research.
-
The DSD Schema Language
(With Michael I. Schwartzbach and Anders Møller, Automated
Software Engineering Journal, 9(3): 285-319; Aug 2002)
DSD (Document Structure Description), an XML grammar
formalism. DSDs are generally more expressive than XML
Schema, provide a useful CSS-like default mechanism, and are
defined in about 15 pages—as opposed to close to 200 for XML
Schema.
-
Towards SMIL as a foundation
for multimodal, multimedia applications. (With
Jennifer Beckham and Gioseppe di Fabbrizio)
Eurospeech '01, 2001.) A basic
programming-language framework is suggested to cope
with difficult issues in design of advanced
interactive content.
-
A
Domain-Specific Language for Regular Sets of Strings and
Trees. (With Michael I. Schwartzbach, IEEE TSE, 1999.)
A high-level language based on a kind of predicate logic
for expressing regular sets. The notation extends Monadic
Second-order Logic with types and other abstractions found
in programming languages.
-
YakYak:
Parsing with Logical Side Constraints . (With Niels
Damgaard and Michael
I. Schwartzbach, Proc. Developments in Language
Theory, 1999.) On extending Yacc with first-order
logic for specifying constraints that are regular tree
languages.
-
Automatic
Verification of Pointer Programs using Monadic
Second-order Logic . (With Michael I. Schwartzbach,
PLDI '97 1997.) A decidable Hoare logic for a
fragment of Pascal that includes pointers and while
loops. Using a decision procedure, we can answer detailed
questions about pointer usage automatically.
-
Automated
logical verification based on trace abstractions
. (With Mogens Nielsen and Kim Sunesen,
PODC '96.) A behavioral approach to the
comparison of distributed systems. We formulate proof
principles that can be expressed in M2L and that allow
component-wise verification.
Progress measures
-
Rabin Measures (with
Dexter Kozen. CJTCS, 1995.) Introduction of a
concept for quantifying progress of transitions towards
satisfaction of the Rabin (or pairs) condition. Linked to
the Kleene-Brouwer ordering of recursion theory, these
measures eliminate the need for syntax-dependent,
recursive proof rules for termination problems under
fairness.
-
The Limit View of Infinite
Computations
. (CONCUR '94.) Computations involving
very general liveness properties as limits of finite
approximations. Our results allow us directly to relate
finite computations in order to infer properties about
infinite ones. We relate our work to the Kleene-Suslin
Theorem and Martin's theorem about determinacy.
- Progress Measures for Complementation of
\omega-Automata with Applications to Temporal Logic
. (FOCS 1991.)
-
Progress Measures, Immediate
Determinacy, and a Subset Construction For Tree Automata.
. (J. Applied Logic, 1994) A proof based on
progress measures of Rabin's fundamental result of closure
of automata-defined languages of infinite, labeled trees.
Earlier constructions yielded doubly-exponential blowups,
but our construction is only exponential.
-
Progress Measures for Fair
Termination. (PODC 1992.)
User interfaces
-
Word
n-grams for cluster keyboards (with Michael Riley,
EACL Workshop on Text Entry, 2003) Experimental studies of
how large language models help in correctly identifying
words entered on keyboards where letters are clustered (such
as on the telephone keypad). A reduced version of the
QWERTY layout appears especially promising.
-
Editing by
Voice and the Role of Sequential Symbol Systems for Improved
Human-to-Computer Information Rates. (ICASSP 2003.)
Arguments based on
cognitive theory, analyses of examples, and empirical
measurements for the potential of constructed jargons as a
solution to inefficacy of conventional spoken command and control.
-
ShortTalk: a proposal for improving
dictation systems. (2002.) A manifesto arguing that
current speech user interfaces for text composition offers
enormous room for improvement, especially if a utilitarian,
no-natural-language attitude is adopted.
-
ShortTalk: an efficient spoken
editing language. (In preparation.) A complete
description of ShortTalk, its philosophy, and
experiments.
-
Input devices: a
usage-driven approach. (2002.) An essay on why
almost every “ergonomic” input device does not work or
is harmful—along with some ideas for devices that may
actually work.
-
A keyboard design.
(2001.) Various minor suggestions for improving the keyboard.
printer-friendly version
e-mail Klarlund
Nils
Klarlund home