TeX Analysis System (TeXAS)
TeX (and its LaTeX incarnation) is a widely used document preparation system for technical and scientific documents. At the same time, TeX is also an unusual programming language with a quite powerful macro system.
The motivation for the TeXAS project is that the behavior of TeX is considerably hard to predict, it is difficult to trace errors back to their causes, and it is hard to write macros that are “well-behaved”. In particular, even syntactic errors occur while running TeX, because TeX is a dynamically parsed language.
The goal of the TeXAS project is to remedy this problem by developing:
- A formal semantics for TeX which makes the language fully predictable.
- A parser that enables the detection of syntactic errors prior to executing TeX itself and is guaranteed to terminate. The resulting abstract syntax trees can then form the basis of more advanced syntax-directed analyses and transformations.
- A type system supporting the deduction of static guarantees about the usages of primitives and macros in TeX.
- The degree of automation of typechecking should be as high as possible. The current idea is to use something alike Hindley-Milner type inference plus extensions for TeX’s primitives. In those cases where full automation is not possible, the macros could either be annotated with typing information, or (in hopefully) rare cases the macros have to be rewritten. To identify the common cases, we intend to analyze existing macro libraries.
Another, more long-term goal, of the project is to redesign the core of TeX, e.g. replace its macro language by (statically) typed functions, make the grammar of TeX context-free, relax various ad hoc restrictions, etc. The above described type checker will hopefully enable a smooth migration to the redesigned core.
Sebastian Thore Erdweg and Klaus Ostermann. Featherweight TeX and Parser Correctness. In Proc. Int'l Conf. Software Language Engineering (SLE), Lecture Notes in Computer Science. Springer, 2010. to appear. [ abstract | bib | .pdf ]