Research themes
|
XML research
survey.
(draft version). XML: Model,
Schemas, Types, Logics and Queries (with Thomas
Schwentick and Dan Suciu), revised version to appear in
Logics of emerging applications of databases,
Eds. J. Chomicki, G. Saake, and R. van der Meyden,
Springer Verlag, 2003. Related invited talk
at NICTA Inaugural Formal Methods Programme Workshop.
|
|
Language
modeling for typing on Q14 and other reduced
keyboards.
We show that the word error rate for
typing on a keyboard where adjacent keys have been
clustered in pairs according to the QWERTY layout may be
made almost negligible thanks to large language models
used in speech recognition. The keyboard is now available
on the BlackBerry 7100.
|
|
ShortStep
foot keyboard design.
A radically different
approach to managing computer-related discomfort.
Almost every keyboard shortcut is directly accessible
through foot keys. The ShortStep keyboard allows
you to lean back in your chair while working on
repetitive tasks with little or no use of your arms.
Concept and software
are hosted at SourceForge.
|
|
Making decades-old theory linking automata and
logic work in practice.
The concept of BDD for encoding Boolean functions
plays an important role in verification. Mona is a
tool based on a more general theory related to
decidable fragments of arithmetic. Applications of
Mona include hardware verification, protocol
configuration, pointer analysis, parsing, theorem
proving, etc.
|
|
Towards a foundation for multimodal, multimedia
content definition.
Multimedia content—where
audio, video, and graphics—are synchronized in
sophisticated ways is already common on the Web.
Multimodal interfaces extend usability by integrating
speech recognition, gestures, etc. A foundation for
such work must be based on a programming language that
includes concurrency, timing constraints, and built-in
undo support. The survey talk (html) [Powerpoint] explains my
interests in user interface technology and how they lead to
fundamental questions about events and synchronicity.
|
|
Editing
talk so enticingly efficient it is a pleasure to
learn.
Speech recognition as a way of getting your thoughts
across the human-machine interface remains an elusive
technology. ShortTalk solves the problem in the domain
of text composition though a constructed editing
language. Slides
from talk:
ShortTalk and ShortStep—with mid-20th century insights
into universal and perfect languages. ShortTalk paper presented
at ICME '2003 (also,
ICASSP '2003). Now
available
at SourceForge as open speech
software offered by Carnegie Mellon University.
|
|
Usage-driven design.
Since overuse injury is a long-term result, most
"ergonomic" design remains unproven—despite claims of
positive results in trials. I have experimented with
input device concepts for over 10 years. It is my hope
that the couple of surviving ideas may help other people
suffering from computer-induced pain.
|
|
The essentials of XML
Clogged by
contradictory and complex specifications, XML at heart
is a welcome practical manifestation of tested ideas in
computer science. With the DSD work, we try to
influence the XML community through proposals rooted in
programming language and automata theory. DSD 2.0
by Anders Møller can be found at the
DSD Web site.
|
|
Understanding infinite computations in terms of
finite ones.
In my Ph.D. thesis, I argued that infinite computations
that involve liveness are best understood as limits of
finite ones. The finite approximations are
characterized by a progress value. For various levels
of topological complexity, it is possible to formulate
such measures of progress. Applications include
reasoning about fairness and analyses of automata on
infinite objects.
|
Publications
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.
Clairgrove
Clairgrove LLC
develops intellectual property in select areas of computer
science.
My workspace: speech recognition and foot keyboard
My computer workspace is an unusual one. It is designed
with the goal of virtually eliminating the usual physical
strain on fingers, hands, and arms. Therefore, the use of
these body parts must be drastically reduced—something that
no amount of tinkering with keyboard or mouse design can
achieve. The other goal is that the reassigned workspace be
more efficient the conventional one; otherwise, there is no
incentive to start working in different ways. These goals are
usually regarded as irreconcilable. Attempting to solve
the problem, I have been motivated by a typing injury (for
that story see CTD-RSI).
After ten years of trial and error, I believe that I have
found a promising approach. The solution is not
commercially available. And, I don't know to which extent
my ideas apply in general for the many people who are unable
to use the keyboard and mouse in the intensive way
necessitated by modern jobs.
My low-impact workspace concept integrates three user
interface ideas:
- replace the keyboard with speech recognition for
dictation and editing;
- defer repetitive work to foot pedals; and
- replace the mouse with a buttonless pointing device
that is pushed around on a large surface.
The physical expression of this concept can be seen in this picture:
The video demos demonstrate how composing a letter is a
breeze with speech recognition and how repetitive tasks are
accomplished easily by foot work.
- The video ShortTalk for composing a
business letter (streaming AVI format) [mpeg-1 version (12Mb)]
shows how speech recognition serves two roles efficiently:
that of automated transcription into a text editor and
that of editing the resulting text through the use of ShortTalk. The editing
commands of ShortTalk are those words that sound unusual:
they must be different from English, since that is the
only way to fluently mix dictation and commands
(otherwise, how would the machine know what is what?).
ShortTalk is several times more efficient than the
so-called natural language commands of commercial
dictation systems.
- The video foot
keyboard (WMW, streaming Windows Media) [mpeg-1 version (28Mb)]
shows how all the keys that are commonly used for repetitive
tasks can be activated by feet through a foot rest
surrounded by switches. The foot keyboard effectively
complements speech recognition, since it relieves the
voice of tiring work for which it is not suited. For more
information, see Input
devices: a usage-driven approach.
With the techniques illustrated in the videos, it is
possible to work while leaning backwards in a relaxed
manner, since hand work and finger work has been reduced to
just occasionally pushing the mouse around. Therefore, the
workplace puts less stress on neck and back as well.
Curriculum Vitae
Brief Vita
Nils Klarlund is the founder of Clairgrove LLC. Presently
a research scientist at Google, Nils Klarlund has worked at
IBM TJ Watson Research Center, the University of Aarhus,
AT&T Labs--Research, and Lucent Bell Labs. His interests
span user interface design, reactive programming languages,
algorithms for symbolic analysis, and program testing and
verification. He received a M.Sc. from the University of
Aarhus and a Ph.D in Computer Science from Cornell
University.
CV
A CV is available in PDF: here.
By Nils Klarlund.
Copyright ©Nils Klarlund, 2003.
|
XSLT &
|