# Grammatical Framework Bibliography

### Publications on GF

In reverse temporal order:

D. A. Burke and K. Johannisson. "Translating Formal Software Specifications to Natural Language / A Grammar-Based Approach". In Logical Aspects of Computational Linguistics (LACL 2005), ed. by P. Blace, E. Stabler, J. Busquets and R. Moot, Springer LNAI 3402, pp. 51-66, 2005.
A paper explaining how a multilingual GF grammar is completed with Natural Language Generation techniques to improve text quality.

Björn Bringert, Robin Cooper, Peter Ljunglöf, Aarne Ranta, Multimodal Dialogue System Grammars [abstract, paper (pdf), paper (ps), bibtex, slides (pdf)], in Proceedings of DIALOR'05, Ninth Workshop on the Semantics and Pragmatics of Dialogue, Nancy, France, June 9-11, 2005.
Shows how mouse clicks can be integrated in GF grammars alongside with speech input.

Kristofer Johannisson, Formal and Informal Software Specifications. PhD thesis, Computer Science, Göteborg University, 2005.

A. Ranta, "Modular Grammar Engineering in GF". Available in pdf. A later version to appear in Research in Language and Computation, 2005.
Argues for library-based software engineering methods in grammar writing and introduces the module system of GF.

P. Ljunglöf. Expressivity and Complexity of the Grammatical Framework. PhD thesis, Computer Science, Göteborg University, 2004.
Language-theoretical study of GF and its parsing problem.

A. Ranta, "Grammatical Framework. A Type-Theoretical Grammar Formalism". Article appeared in The Journal of Functional Programming, vol. 14:2. 2004, pp. 145-189. Earlier version available in gzipped postscript.
Theoretical paper explaining the GF formalism and its implementation. Aimed to be the standard reference on GF, but doesn't cover the module system.

A. Ranta, "Computational Semantics in Type Theory". Mathematics and Social Sciences, 165:31-57, 2004 An earlier version appeared as course material for graduate course in computational linguistics, Gothenburg University, 2001. Available in gzipped postscript.
Shows how PTQ-style grammars are implemented in GF and extends this to type-theoretical grammars for anaphoric expressions.

H. Hammarström and A. Ranta. Cardinal Numerals Revisited in GF. Workshop on Numerals in the World's Languages. Dept. of Linguistics Max Planck Institute for Evolutionary Anthropology, Leipzig, Germany, 2004.
An overview of the numeral grammar project.

A. Ranta. Grammatical Framework Tutorial. In A. Beckmann and N. Preining, editors, ESSLLI 2003 Course Material I, volume V of Collegium Logicum, pages 1-86. Kurt Gödel Society, 2004.
A revised version of the on-line GF tutorial.

J. Khegai and A. Ranta. "Building and using a Russian Resource Grammar in GF". In Intelligent Text Processing and Computational Linguistics (CICLing-2004), Seoul, Korea. LNCS, pages 38-41. Springer, 2004.
An introduction to the GF resource grammar project, with Russian as prime example.

A. Ranta and R. Cooper, "Dialogue Systems as Proof Editors". Journal of Logic, Language and Information, 13:225-240, 2004. An earlier version appeared in IJCAR/ICoS-3, Siena, June 2001. Available in gzipped postscript.

J. Khegai, B. Nordström, and A. Ranta. "Multilingual Syntax Editing in GF", In Intelligent Text Processing and Computational Linguistics (CICLing-2003), ed. by A. Gelbukh, Springer LNCS 2588, pp. 453-464. Available in gzipped postscript.
Explains how the GF GUI is used in syntax editing and discusses how new grammars are created.

R. Hähnle, K. Johannisson, and A. Ranta. "An Authoring Tool for Informal and Formal Requirements Specifications". In ETAPS/FASE-2002: Fundamental Approaches to Software Engineering, ed. by R. D. Kutsche and H. Weber, Springer LNCS, vol. 2306, pp. 233--248, 2002. Available in pdf.
Describes a GF-based authoring tool for object-oriented specifications in OCL and English. Carries out in full the work proposed in the position paper (Hähnle & Ranta 2001).

K. Johannisson and A.Ranta, "Formal Verification of Multilingual Instructions", Proceedings of the Joint Winter Meeting 2001 of the Departments of Computer Science and Computer Engineering, Chalmers University of Technology and Göteborg University. Available in gzipped postscript.
Instructions for an alarm system in four languages, verified in the proof editor Alfa.

R. Hähnle and A. Ranta, "Connecting OCL with the Rest of the World", ETAPS 2001 Workshop on Transformations in UML (WTUML), Genova, 2001. Available in gzipped postscript.
A position paper explaining how GF can be used to help in object-oriented modelling, with some examples on natural-language interaction with OCL (Object Constraint Language).

T. Hallgren, "The Correctness of Insertion Sort", Manuscript, Chalmers University, Göteborg, 2001. Available in postscript.
A seven-page text generated by GF-Alfa.

A. Ranta. "Bescherelle bricolé", gzipped postscript, 2001.
A machine-generated book on French conjugation implemented in GF.

T. Hallgren and A. Ranta, "An Extensible Proof Text Editor". M. Parigot & A. Voronkov (eds), Logic for Programming and Automated Reasoning (LPAR'2000), LNCS/LNAI 1955, pp. 70-84, Springer Verlag, Heidelberg, 2000. Available in gzipped postscript.
Describes an interface to the proof editor Alfa written in GF.

M. Dymetman, V. Lux, and A. Ranta, "XML and multilingual document authoring: converging trends", Proceedings of the The 18th International Conference on Computational Linguistics (COLING 2000), pp. 243-249, Saarbruecken, 2000. Available in gzipped postscript.
Relates GF not only with XML but also with definite clause grammars.

P. Mäenpää and A. Ranta. The type theory and type checker of GF. Colloquium on Principles, Logics, and Implementations of High-Level Programming Languages, Workshop on Logical Frameworks and Meta-languages, Paris, France, 28 September 1999. Available in gzipped postscript.
Concise theoretical presentation of GF, using the old notation..

### Background for GF

In alphabetical order:

L. Magnusson. The Implementation of ALF - a Proof Editor based on Martin-Löf's Monomorphic Type Theory with Explicit Substitutions. PhD Thesis, Department of Computing Science, Chalmers University of Technology and Göteborg University, 1994.
Back in 1992 the most wonderful program in the world, ALF is a model that GF directly follows: GF is Yet ALF.

P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984.
A very accessible book (if you have access to it!) on type theory directly from the source.

B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory: an Introduction. Oxford University Press, 1990. The book is out of print, but a free version can be picked up from www.cs.chalmers.se/Cs/Research/Logic/book/
Standard reference on the subject.

A. Ranta. Type Theoretical Grammar. Oxford University Press, Oxford, 1994. Publisher's information.
Monograph on type theory in linguistics. Includes an introduction to type theory. Much focused on anaphora. A first, very rudimentary implementation of syntax in the proof system ALF.

A. Ranta. Syntactic categories in the language of mathematics. P. Dybjer, B. Nordström, and J. Smith, eds., Types for Proofs and Programs, pp. 162-182, Lecture Notes in Computer Science 996, Springer-Verlag, Heidelberg, 1995.
Predecessor of GF: grammar defined in type theory and implemented in ALF.

A. Ranta. Context-relative syntactic categories and the formalization of mathematical text. S. Berardi and M. Coppo, eds., Types for Proofs and Programs, pp. 231-248, Lecture Notes in Computer Science 1158, Springer-Verlag, Heidelberg, 1996.
Extending the theory of the previous paper. The implementation in ALF eventually became so heavy that the need arose for GF.

A. Ranta. Structures grammaticales dans le français mathématique. Mathématiques, informatique et Sciences Humaines., vol. 138 pp. 5-56 and 139 pp. 5-36, 1997.
A rather comprehensive French grammar presented in a type-theoretical style.

A. Ranta. Syntactic calculus with dependent types. Journal of Logic, Language and Information, vol. 4, pp. 413-431, 1998.
Interprets Lambek Calculus in type theory and defines some extensions.