From 5e5c613f7ef90c7b9d71cf7535511158adc2dc11 Mon Sep 17 00:00:00 2001
From: aarne
+
+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.
+
+
+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.
+
+
+T. Hallgren, "The Correctness of Insertion Sort",
+Manuscript, Chalmers University, Göteborg, 2001.
+Available in
+
+postscript.
+
+
+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.
+
+
+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.
+
+
+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.
+
+
+
+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.
+
+
+A. Ranta,
+"Grammatical Framework. A Type-Theoretical Grammar Formalism".
+Manuscript, 2002.
+Available in
+
+ gzipped postscript.
+Article appeared in The Journal of Functional Programming, vol. 14:2. 2004, pp. 145-189.
+
+
+A. Ranta,
+ "Computational Semantics in Type Theory".
+ Course material for graduate course in computational linguistics,
+ Gothenburg University, 2001.
+Available in
+
+ gzipped postscript.
+
+
+A. Ranta and R. Cooper,
+ "Dialogue Systems as Proof Editors".
+ IJCAR/ICoS-3, Siena, June 2001.
+Available in
+
+ gzipped postscript. A later version appeared in
+Journal of Logic, Language and Information, 13:225-240, 2004
+
+
+
+A. Ranta,
+ "Modular Grammar Engineering in GF".
+Available in
+
+ pdf. A later version to appear in
+ Research in Language and Computation, 2005.
+
+
+A. Ranta. "Bescherelle bricolé",
+gzipped postscript, 2001.
+
+
+
+
+
+
+
+P. Martin-Löf.
+Intuitionistic Type Theory.
+Bibliopolis, Naples, 1984.
+
+
+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/
+
+
+A. Ranta.
+ Type Theoretical Grammar.
+ Oxford University Press, Oxford, 1994.
+Publisher's information.
+
+
+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.
+
+
+
+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.
+
+
+
+ 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. Ranta.
+ Syntactic calculus with dependent types.
+ Journal of Logic, Language and Information, vol. 4,
+ pp. 413-431, 1998.
+
-
+
November 8, 2004. GF 2.1 released.
Here are the highlights.
Software available on the GF 2.1 Download
Page.
-
Main novelties in 2.1:
multiple inheritance of grammar modules,
speech recognition grammar generation,
lots of bug fixes.
-
-
-
Version 2.0 still available
on the GF 2.0 Download Page.
-
-
-
If you need something from the previous version of the web page, it is
still available:
GF 1.2.
-
+
+
+GF grammars can be embedded in Java programs by using the
+Embedded GF Interpreter.
+
+
+Grammatical Framework Bibliography
+Publications on 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.
+
+
+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).
+
+
+
+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).
+
+
+A seven-page text generated by GF-Alfa.
+
+
+Describes an interface to the proof editor Alfa written in GF.
+
+
+Instructions for an alarm system in four languages, verified in the
+proof editor Alfa.
+
+
+
+Explains how the GF GUI is used in syntax editing and discusses
+how new grammars are created.
+
+
+
+Concise theoretical presentation of GF, using the old notation..
+
+
+Theoretical paper explaining the GF formalism and its
+implementation. Aimed to be the work of reference on GF.
+
+
+
+ Shows how PTQ-style grammars are implemented in GF and extends
+this to type-theoretical grammars for anaphoric expressions.
+A later version appeared in
+Mathematics and Social Sciences, 165:31-57, 2004
+
+
+Argues for library-based software engineering methods in grammar writing and introduces
+the module system of GF.
+
+
+A machine-generated book on French conjugation implemented in GF.
+
+Background for GF
+
+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.
+
+
+A very accessible book (if you have access to it!)
+on type theory directly from the source.
+
+
+Standard reference on the subject.
+
+
+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.
+
+
+Predecessor of GF: grammar defined in type theory and implemented
+in ALF.
+
+
+Extending the theory of the previous paper.
+The implementation in ALF eventually became so heavy that
+the need arose for GF.
+
+
+
+A rather comprehensive French grammar presented in a type-theoretical
+style.
+
+
+Interprets Lambek Calculus in type theory and defines some
+extensions.
+
+
+
+
+
+
diff --git a/index.html b/index.html
index 7ba2f45fd..696f2d570 100644
--- a/index.html
+++ b/index.html
@@ -1,5 +1,5 @@
-Source code
@@ -186,7 +183,6 @@ information on compiler requirements.
- -KeY project on Integrated Deductive +
- -WebALT, +
- +
- +