Featherweight TEX and parser correctness

Abstract

(and its incarnation) is a widely used document preparation system for technical and scientific documents. At the same time, is also an unusual programming language with a quite powerful macro system. Despite the wide range of users (especially in the scientific community), and despite a widely perceived considerable level of "pain" in using , there is almost no research on . This paper is an attempt to change that. To this end, we present Featherweight , a formal model of which we hope can play a similar role for as Featherweight Java did for Java. The main technical problem which we study in terms of Featherweight is the parsing problem. As for other dynamic languages performing syntactic analysis at runtime, the concept of "static" parsing and its correctness is unclear in and shall be clarified in this paper. Moreover, it is the case that parsing is impossible in general, but we present evidence that parsers for practical subsets exists. We furthermore outline three immediate applications of our formalization of and its parsing: a macro debugger, an analysis that detects syntactic inconsistencies, and a test framework for parsers. © 2011 Springer-Verlag Berlin Heidelberg.