Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-66644f4456-xp6jp Total loading time: 0 Render date: 2025-02-13T02:46:32.347Z Has data issue: true hasContentIssue false

12 - Towards a theory of document structure

Published online by Cambridge University Press:  06 August 2010

By
Bengt Nordström
Edited by
Yves Bertot ,
Gérard Huet ,
Jean-Jacques Lévy  and
Gordon Plotkin
Bengt Nordström
Affiliation:
Chalmers University of Technology and the University of Göteborg
Yves Bertot
Affiliation:
INRIA-Sophia Antipolis, France
Gérard Huet
Affiliation:
Institut National de Recherche en Informatique et en Automatique (INRIA), Rocquencourt
Jean-Jacques Lévy
Affiliation:
Institut National de Recherche en Informatique et en Automatique (INRIA), Rocquencourt
Gordon Plotkin
Affiliation:
University of Edinburgh
Get access

Summary

Abstract

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.

Type
Chapter
Information
From Semantics to Computer Science
Essays in Honour of Gilles Kahn
 , pp. 265 - 280
Publisher: Cambridge University Press
Print publication year: 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

[1],Agda homepage. unit.aist.go.jp/cvs/Agda/.
[2]A., Asperti, G., Bancerek and A., Trybulec (eds). Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings, volume 3119, Lecture Notes in Computer Science. Springer, 2004.Google Scholar
[3]R., Bornat and B., Sufrin. Animating formal proof at the surface: The Jape proof calculator. Computer Journal, 42(3):177–192, 1999.Google Scholar
[4]P., Borras, D., Clement, Th., Despeyrouz, J., Incerpi, G., Kahn, B., Lang, and V., Pascual. CENTAUR: The system. In Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments (PSDE), volume 24, pp. 14–24, New York, NY, 1989. ACM Press.Google Scholar
[5],Coq homepage. pauillac.inria.fr/coq/, 1999.
[6]H. B., Curry. Some logical aspects of grammatical structure. In R. O., Jakobson (ed.) Structure of Language in its Mathematical Aspects. Proceedings of the 12th Symposium in Applied Mathematics, pp. 56–68, 1961.Google Scholar
[7]V., Donzeau-Gouge, G., Huet, G., Kahn and B., Lang. Programming environments based on structured editors: The MENTOR experience, 1984.
[8],Eclipse homepage. www.eclipse.org.
[9]T., Hallgren. Alfa homepage. www.cs.chalmers.se/∼hallgren/Alfa/, 1996–2000.
[10]J., Harrison. The HOL light theorem prover. www.cl.cam.ac.uk/∼jrh13/hol–light/, 2006.
[11]G., Huet and G., Plotkin (eds) Logical Frameworks: First International Workshop on Logical Frameworks, Antibes, May, 1990. Cambridge University Press, 1991.Google Scholar
[12]G., Huet and G., Plotkin (eds) Logical Environments: Second International Workshop on Logical Frameworks, Edinburgh, May, 1991. Cambridge University Press, 1993.Google Scholar
[13],Isabelle Homepage. www.cl.cam.ac.uk/Research/HVG/Isabelle/, 2003.
[14]D. E., Knuth. Literate Programming. CSLI, 1992.Google Scholar
[15]L., Magnusson and B., Nordström. The ALF proof editor and its proof engine. In Types for Proofs and Programs, volume 806, Lecture Notes in Computer Science, pp. 213–237, Nijmegen, 1994. Springer-Verlag.Google Scholar
[16]P., Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.Google Scholar
[17]B., Nordström, K., Petersson and J. M., Smith. Martin-Löf's Type Theory, chapter 1, pp. 1–33. Oxford University Press, 2001.Google Scholar
[18]L., Padovani and R., Solmi. An investigation on the dynamics of direct-manipulation editors for mathematics. In Asperti et al. [2], pp. 302–316.
[19]R., Pollack. The LEGO proof assistant. www.dcs.ed.ac.uk/home/lego/, 1997.
[20]A., Ranta. Grammatical Framework Homepage. www.cs.chalmers.se/∼aarne/GF/, 1999–2005.
[21]A., Ranta. Grammatical Framework: A Type-Theoretical Grammar Formalism. Journal of Functional Programming, 14(2):145–189, 2004.Google Scholar
[22],The Types Project Homepage. www.cs.chalmers.se/Cs/Research/Logic/Types/.
[23]L., Théry, Y., Bertot and G., Kahn. Real theorem provers deserve real user-interfaces. In Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments, pp. 120–129, 1992.Google Scholar

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×