Towards a theory of document structure
Bengt Nordström · Cambridge University Press eBooks · 2009
The structure of documents of various degree of formality, from scientific papers with layout information and programs with their documentation to completely formal proofs can be expressed by assigning a type to the abstract syntax tree of the document. By using dependent types – an idea from type theory – it is possible to express very strong syntactic criterion on wellformedness of documents. This structure can be used to automatically generate parsers, type checkers and structure-oriented editors. Introduction We are interested to find a general framework for describing the structure of many kinds of documents, such as books and articles “live” documents (like a web document with parts to be filled in) programs formal proofs. Are there any good reasons why we use different programs to edit and print articles, programs and formal proofs? A unified view on these kinds of documents would make it possible to use only one structure-oriented editor to build all of them, and it would be easier to combine documents of different kinds, for instance scientific papers, programs with their documentation, informal and formal proofs and simple web forms. Such a view requires that we have a good framework to express syntactic wellformedness (from things like the absence of a title in a footnote to correctness of a formal proof) and to express how the document should be edited and presented.