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 logicautomaton connection. (Submitted.) The
mathematical framework Mona uses for handling firstorder
variables and relativizations. This paper introduces
ternary and sexpartite valuations to capture relativized
formulas under an automatatheoretic view.

An n log n algorithm for
online BDD refinement. (J. of Alg., 1999.) A
minimization construction for BDDrepresented
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 monadicsecondorder 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): 285319; Aug 2002)
DSD (Document Structure Description), an XML grammar
formalism. DSDs are generally more expressive than XML
Schema, provide a useful CSSlike 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
programminglanguage framework is suggested to cope
with difficult issues in design of advanced
interactive content.

A
DomainSpecific Language for Regular Sets of Strings and
Trees. (With Michael I. Schwartzbach, IEEE TSE, 1999.)
A highlevel language based on a kind of predicate logic
for expressing regular sets. The notation extends Monadic
Secondorder 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 firstorder
logic for specifying constraints that are regular tree
languages.

Automatic
Verification of Pointer Programs using Monadic
Secondorder 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
componentwise 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 KleeneBrouwer ordering of recursion theory, these
measures eliminate the need for syntaxdependent,
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 KleeneSuslin
Theorem and Martin's theorem about determinacy.
 Progress Measures for Complementation of
\omegaAutomata 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 automatadefined languages of infinite, labeled trees.
Earlier constructions yielded doublyexponential blowups,
but our construction is only exponential.

Progress Measures for Fair
Termination. (PODC 1992.)
User interfaces

Word
ngrams 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
HumantoComputer 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,
nonaturallanguage attitude is adopted.

ShortTalk: an efficient spoken
editing language. (In preparation.) A complete
description of ShortTalk, its philosophy, and
experiments.

Input devices: a
usagedriven 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.