Nils Klarlund PhD, Cornell University, 1990

	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.

• MON Implementation Secrets. (International Journal of Foundations of Computer Science, Vol. 13, No. 4 (2002).) An overview of the techniques used in the MONA tool. The respective effects of the techniques are quantified by experiments on a number of benchmarks.
• MONA v1.4 User Manual (PDF)
• Mona & Fido: The Logic-Automaton Connection in Practice (PostScript). (Computer Science Logic '97, invited paper, 1997.) An gentle introduction to the automata-logic connection.
• Mona tutorial, automata-based symbolic computation (PDF). (2001.) (A PostScript version is also available.). Slides for a Mona tutorial.

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

• ECLIPSE Feature Logic Analysis. (IP-telephony Workshop, 2001.) Verification applied to advanced IP-telephony services.
• Verification of a Sliding Window Protocol Using IOA and MONA. (With Mark Smith. FORTE/PSTV, 2000.) Automatic verification of an unbounded, sliding window protocol.
• Automata based symbolic reasoning in hardware verification . (With David Basin. FMSD, 1998.) Hardware verification based on formulating circuits and their specifications in M2L. We use Mona to verify parameterized circuits without induction, and we explain why it works.

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

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 &