GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-10 21:39:32 -06:00
Code Issues Packages Projects Releases Wiki Activity
Files
df4f4bcd6fa052d476adc6bc9848d29d954a1b34
gf-core/doc/gf-bib.bib
aarne f5519f77eb paper and references
2004-09-26 16:05:36 +00:00

2100 lines
60 KiB
BibTeX
Raw Blame History

@STRING{fac = "Formal Aspects of Computing"}
@STRING{amai = "Annals of Mathematics and Artificial Intelligence"}
@STRING{jsl = "Journal of Symbolic Logic"}
@STRING{jsc = "Journal of Symbolic Computation"}
@STRING{jlc = "Journal of Logic and Computation"}
@STRING{jlp = "Journal of Logic Programming"}
@STRING{JFP = "Journal of {F}unctional {P}rogramming"}
@STRING{jar = "Journal of Automated Reasoning"}
@STRING{sl = "Studia Logica"}
@STRING{ipl = "Information Processing Letters"}
@STRING{tcs = "Theoretical Computer Science"}
@STRING{lnm = "Lecture Notes in Mathematics"}
@STRING{lncs = "LNCS"}
@STRING{lnai = "LNCS"}
@STRING{spv = "Springer-Verlag"}
@STRING{cacm = "Communications of the {ACM}"}
@STRING{jacm = "Journal of the {ACM}"}
@STRING{sc = "Soft Computing---A Fusion of Foundations, Methodologies
and Applications"}
@article{KeY2004,
author = {Wolfgang Ahrendt and Thomas Baar and
Bernhard Beckert and Richard Bubel and
Martin Giese and Reiner H\"ahnle and
Wolfram Menzel and Wojciech Mostowski and
Andreas Roth and Steffen Schlager and
Peter H. Schmitt},
title = {The {KeY} Tool},
journal = {Software and System Modeling},
year = {2004},
note = {Online First issue, to appear in print}
}
@ARTICLE{landin,
AUTHOR = "P. Landin",
TITLE = "The Next 700 Programming Languages",
JOURNAL = {{Communications of the ACM}},
VOLUME = {9},
PAGES = {157--166},
YEAR = {1966}
}
@techreport{KeY2003,
author = {Wolfgang Ahrendt and Thomas Baar and
Bernhard Beckert and Richard Bubel and
Martin Giese and Reiner H\"ahnle and
Wolfram Menzel and Wojciech Mostowski and
Andreas Roth and Steffen Schlager and
Peter H. Schmitt},
title = {The KeY Tool},
institution = {Department of Computing Science, Chalmers University
and G\"oteborg University, G\"oteborg, Sweden},
type = {Technical Report in Computing Science No.\ 2003-5},
month = feb,
year = {2003}
}
@ARTICLE{copestake,
AUTHOR = "A. Copestake and D. Flickinger",
TITLE = "An open-source grammar development environment and broad-coverage English grammar using HPSG",
JOURNAL = {{Proceedings of the Second conference on Language Resources and Evaluation (LREC-2000)}},
YEAR = {2000}
}
@book{pereira-shieber,
AUTHOR = {F. Pereira and S. Shieber},
TITLE = {{Prolog and Natural-Language Analysis}},
ADDRESS = {Stanford},
YEAR = {1987},
PUBLISHER = {{CSLI}}
}
@book{aho-ullman,
AUTHOR = {A. Aho and R. Sethi and J. Ullman},
TITLE = {{Compilers: Principles, Techniques, and Tools}},
YEAR = {1988},
PUBLISHER = {{Addison-Wesley}}
}
@book{martin-lof,
AUTHOR = {P. Martin-L\"{o}f},
TITLE = {{Intuitionistic Type Theory}},
ADDRESS = {Napoli},
YEAR = {1984},
PUBLISHER = {Bibliopolis}
}
@BOOK{curry,
AUTHOR = "Curry, H. B. and R. Feys",
TITLE = "Combinatory Logic, Vol. 1",
PUBLISHER = {North-Holland},
ADDRESS = {Amsterdam},
YEAR = {1958} }
@ARTICLE{scott-str,
AUTHOR = "D. S. Scott and C. Strachey",
TITLE = "Toward a mathematical semantics for computer languages",
JOURNAL = {Microwave Research Institute Symposia Series},
VOLUME = {21},
PAGES = {19--46},
YEAR = {1970} }
@ARTICLE{partee,
AUTHOR = {B. Partee},
TITLE = {Montague grammar and transformational grammar},
JOURNAL = {{Linguistic Inquiry}},
VOLUME = {6},
PAGES = {203--300},
YEAR = {1975} }
@Book{ttg,
author = {A. Ranta},
title = {Type Theoretical Grammar},
publisher = {Oxford University Press},
year = {1994}
}
@Book{b-b,
author = {P. Blackburn and J. Bos},
title = {Representation and Inference for Natural Language},
publisher = {Studies in Logic, Language, and Information, CSLI Press},
year = {to appear}
}
@Book{cooper,
author = {R. Cooper},
title = {Quantification and Syntactic Theory},
publisher = {D. Reidel},
year = {1981}
}
@Book{jasmin,
author = {J. Meyer and T. Downing},
title = {{Java Virtual Machine}},
publisher = {O'Reilly},
year = {1997}
}
@Misc{gf,
author = {A. Ranta},
title = {{\mbox{Grammatical Framework Homepage}}},
howpublished = {\verb!http://www.cs.chalmers.se/~aarne/GF/!},
documentURL = {"http://www.cs.chalmers.se/~aarne/GF/"},
year = {2000--2003}
}
@Misc{bnfc,
author = {M. Forsberg and A. Ranta},
title = {{\mbox{BNF Converter Homepage}}},
howpublished = {\verb!http://www.cs.chalmers.se/~markus/BNFC/!},
documentURL = {"http://www.cs.chalmers.se/~markus/BNFC/"},
year = {2002--2004}
}
@Misc{twelf,
author = {F. Pfenning},
title = {{The Twelf Project}},
howpublished = {\verb!http://www-2.cs.cmu.edu/~twelf!},
documentURL = {"http://www-2.cs.cmu.edu/~twelf"},
year = {2002}
}
@INCOLLECTION{scott,
AUTHOR = "D. S. Scott",
TITLE = "Advice on modal logic",
booktitle = {Philosophical Problems in Logic},
EDITOR = {K.\ Lambert},
publisher = {D. Reidel},
YEAR = {1970} }
@BOOK{nordstrom,
AUTHOR = "{Nordstr\"{o}m}, B. and K. Petersson and J. Smith",
TITLE = "Programming in {Martin-L\"{o}f}'s Type Theory. An Introduction",
PUBLISHER = {Clarendon Press},
ADDRESS = {Oxford},
YEAR = {1990} }
@INCOLLECTION{steedman,
AUTHOR = "Steedman, M.",
TITLE = "Combinators and grammars",
EDITOR = "R. Oehrle and E. Bach and D. Wheeler",
BOOKTITLE = "Categorial Grammars and Natural Language Structures",
PUBLISHER = {D. Reidel},
ADDRESS = {Dordrecht},
YEAR = {1988},
PAGES = {417-442}}
@INCOLLECTION{friedman,
AUTHOR = "Friedman, J.",
TITLE = "Expressing logical formulas in natural language",
EDITOR = "J. Groenendijk and T. Janssen and M. Stokhof",
BOOKTITLE = "Formal Methods in the Study of Language, Part 1",
PUBLISHER = {Mathematisch Centrum},
ADDRESS = {Amsterdam},
YEAR = {1981},
PAGES = {113-130}}
@ARTICLE{fri-war,
AUTHOR = "Friedman, J. and D. Warren",
TITLE = "A parsing method for {Montague} grammar",
JOURNAL = {Linguistics and Philosophy},
VOLUME = {2},
PAGES = {347-372},
YEAR = {1978} }
@BOOK{montague,
AUTHOR = "Montague, R.",
TITLE = "Formal Philosophy",
NOTE = {Collected papers edited by Richmond Thomason},
PUBLISHER = {Yale University Press},
ADDRESS = {New Haven},
YEAR = {1974} }
@BOOK{gazdar,
AUTHOR = "Gazdar, G. and E. Klein and G. Pullum and I. Sag",
TITLE = "Generalized Phrase Structure Grammar",
PUBLISHER = {Basil Blackwell},
ADDRESS = {Oxford},
YEAR = {1985} }
@BOOK{chomsky,
AUTHOR = "Chomsky, N.",
TITLE = "Syntactic Structures",
PUBLISHER = {Mouton},
ADDRESS = {The Hague},
YEAR = {1957} }
@Misc{nuance,
author = {{Nuance Communications}},
title = {{Nuance}},
note = {\verb6http://www.nuance.com6},
year = 2002
}
@Article{godis,
author = "S. Larsson and D. Traum",
title = {{Information state and dialogue management in the
TRINDI Dialogue Move Engine Toolkit}},
journal = {{Natural Language Engineering}},
year = 2000,
volume = 0,
pages = 0
}
@BOOK{CLE,
AUTHOR = "Alshawi, H",
TITLE = {{The Core Language Engine}},
PUBLISHER = {{MIT Press}},
ADDRESS = {Cambridge, Ma},
YEAR = {1992} }
@BOOK{cle2,
AUTHOR = {M. Rayner and D. Carter and P. Bouillon and V. Digalakis and
M. Wirén},
TITLE = {{The Spoken Language Translator}},
PUBLISHER = {{Cambridge University Press}},
ADDRESS = {Cambridge},
YEAR = {2000} }
@Article{kaplan-kay,
author = "R. Kaplan and M. Kay",
title = {{Regular Models of Phonological Rule Systems}},
journal = {{Computational Linguistics}},
year = 1994,
volume = 20,
pages = {{331--380}}
}
@inproceedings{Dow:Hoc:Gaw:01,
title = {{Practical Issues in Compiling Typed Unification Grammars
for Speech Recognition}},
author = {J. Dowding and B. A. Hockey and J. M. Gawron
and C. Culy},
booktitle = {{ACL 2001}},
address = {{Toulouse, France}},
year = 2001
}
@BOOK{dowty,
AUTHOR = "Dowty, D",
TITLE = "Word Meaning and Montague Grammar",
PUBLISHER = {D. Reidel},
ADDRESS = {Dordrecht},
YEAR = {1979} }
@Article{metal,
author = "G. Kahn and B. Lang and B. Mélèse and E. Morcos",
title = "Metal: a formalism to specify formalisms",
journal = {Science of {C}omputer {P}rogramming},
year = 1983,
volume = 3,
pages = {151--188}
}
@InCollection{pentus,
author = "M. Pentus",
title = "Lambek grammars are context-free",
booktitle = {{LICS}, {Utrecht}, {The} {Netherlands}},
year = 1993,
pages = {35--42}
}
@ARTICLE{lambek,
AUTHOR = "J. Lambek",
TITLE = "The mathematics of sentence structure",
JOURNAL = {{American Mathematical Monthly}},
VOLUME = {65},
PAGES = {154-170},
YEAR = {1958}
}
@Article{bar-hillel,
author = "Y. Bar-Hillel",
title = "A quasi-arithmetical notation for syntactic description",
journal = {Language},
year = 1953,
volume = 29,
pages = {27-58}
}
@Book{rosetta,
author = {M.~T. Rosetta},
title = {Compositional Translation},
publisher = "Kluwer",
address = "Dordrecht",
year = 1994
}
@Book{hopcroft,
author = {J. Hopcroft and J. Ullman},
title = {{Introduction to Automata Theory, Languages, and Computation}},
publisher = {Addison-Wesley},
year = 1979
}
@Book{jones-partial,
author = {N.D. Jones and C.K. Gomard and P. Sestoft},
title = {{Partial Evaluation and Automatic Program Generation}},
publisher = {Prentice-Hall},
year = 1993
}
@Article{frost,
author = "R. Frost and J. Launchbury",
title = "Constructing natural language interpreters
in a lazy functional language",
journal = {The {Computer} {Journal}},
year = 1989,
volume = 32,
number = 2,
pages = {108--121}
}
@Article{pereira,
author = {H.~D. Warren and F. Pereira},
title = {An Efficient Easily Adaptable System for Interpreting Natural
Language Queries},
year = {1982},
journal = {{Computational Linguistics}},
volume = 8,
pages = {110-122}
}
@Misc{huet-sanskrit,
author = "G. Huet",
title = "Sanskrit site",
howpublished = "Program and documentation,
\verb6http://pauillac.inria.fr/~huet/SKT/6",
documentURL = "\verb6http://pauillac.inria.fr/~huet/SKT/index.html6",
year = 2000
}
@Misc{huet-sanskrit-short,
author = "G. Huet",
title = "Sanskrit site",
howpublished = {\verb6http://pauillac.inria.fr/~huet/SKT/6},
year = 2000
}
@Misc{italiano,
author = "A. Ranta",
title = {1+n representations of {Italian} morphology},
howpublished = {Essays dedicated to {Jan von Plato}
on the occasion of his 50th birthday,
\verb6http://www.valt.helsinki.fi/kfil/jvp50.htm6},
documentURL = "\verb6http://www.valt.helsinki.fi/kfil/jvp50.htm6",
year = 2001
}
@Article{hudak,
author = "P. Hudak",
title = "Building domain-specific embedded languages",
journal = "{ACM} {Computing} {Surveys}",
year = 1996,
volume = 28,
number = 4
}
@Book{bescherelle,
author = "Bescherelle",
title = "La conjugaison pour tous",
publisher = "Hatier",
year = 1997
}
@Book{shieber,
author = "S. Shieber",
title = {{An Introduction to Unification-Based Approaches to Grammars}},
publisher = "University of Chicago Press",
year = 1986
}
@BOOK{prawitz,
AUTHOR = "D. Prawitz",
TITLE = {{Natural Deduction}},
PUBLISHER = {Almqvist \& Wiksell},
ADDRESS = {Stockholm},
YEAR = {1965} }
@BOOK{CAML,
AUTHOR = "P. Weis and X. Leroy",
TITLE = {{Le langage Caml}},
PUBLISHER = {Dunod},
ADDRESS = "Paris",
YEAR = {1999}
}
@BOOK{sml,
AUTHOR = "R. Milner and M. Tofte and R. Harper",
TITLE = {{Definition of Standard ML}},
PUBLISHER = {MIT Press},
YEAR = {1990}
}
@BOOK{ML-wik,
AUTHOR = "{Wikstr\"{o}m}, {\AA ke}",
TITLE = "Functional Programming Using Standard ML",
PUBLISHER = {Prentice-Hall},
ADDRESS = {London},
YEAR = {1987} }
@Article{coquand-typecheck,
author = "T. Coquand",
title = "An Algorithm for Type Checking Dependent Types",
journal = "Science of {Computer} {Programming}",
year = 1996,
volume = 26,
pages = {167-177}
}
@Book{boehm,
author = "H. Barendregt",
title = {{The Lambda Calculus. Its Syntax and Semantics}},
publisher = "North-Holland",
year = 1981
}
@Article{hutton,
author = "G. Hutton",
title = "Higher-order functions for parsing",
journal = {J. Functional Programming},
year = 1992,
volume = 2,
number = 3,
pages = {323--343}
}
@Article{abrusci,
author = "M. Abrusci",
title = {{Noncommutative Intuitionistic Linear Propositional Logic}},
journal = {{Zeitschrift für Mathematische Logik und Grundlagen der Mathematik}},
year = 1990,
volume = 36,
pages = {297--398}
}
@InProceedings{wadler,
author = "P. Wadler",
title = "How to replace failure by a list of successes",
booktitle = {{Second International Conference on Functional
Programming Languages and Computer Architectures}},
series = lncs,
year = 1985,
address = spv
}
@InProceedings{jones-hudak,
author = "M. Jones and P. Hudak",
title = "Using Types to Parse Natural Language",
booktitle = {{Proceedings of the Glasgow Workshop on Functional Programming}},
series = {{LNCS}},
year = 1995,
address = spv
}
@Article{earley,
author = "J. Earley",
title = "An efficient context-free parsing algorithm",
journal = {Communications of the {ACM}},
year = 1970,
volume = 13,
number = 2,
pages = {94--102}
}
@InCollection{joshi,
author = "A. Joshi",
title = {Tree-Adjoining Grammars: How much context-sensitivity is required
to provide reasonable structural descriptions},
booktitle = {{Natural Language Parsing}},
year = 1985,
editor = "D. Dowty and L. Karttunen and A. Zwicky",
publisher = {Cambridge University Press},
pages = {206--250}
}
@Book{appel,
author = {A. Appel},
title = {{Modern Compiler Implementation in ML}},
publisher = {Cambridge University Press},
year = {1998}
}
@Book{prolog,
author = {W. F. Clocksin and C. S. Mellish},
title = {{Programming in Prolog}},
publisher = {Springer},
year = {1984}
}
@Article{hockett,
author = {C. F. Hockett},
title = "Two Models of Grammatical Description",
journal = "Word",
year = 1954,
volume = 10,
pages = {210--233}
}
@Article{Wirth,
author = "N. Wirth",
title = "Program Development by Stepwise Refinement",
journal = "Communications of the ACM",
year = 1971,
volume = 14,
pages = {221--227}
}
@Article{huet-zipper,
author = "G. Huet",
title = {The {Zipper}},
journal = JFP,
year = 1997,
volume = 7,
number = 5,
pages = {549--554}
}
@Article{huet-lang,
author = {G. Huet and B. Lang},
title = {Proving and applying program transformations expressed
with second-order patterns},
journal = {{Acta Informatica}},
year = 1978,
volume = 11
}
@Article{knuth-attr,
author = "D. Knuth",
title = "Semantics of Context-Free Languages",
journal = {Mathematical {Systems} {Theory}},
year = 1968,
volume = 2,
pages = {127--145}
}
@Article{LR,
author = {D. Knuth},
title = {On the translation of languages from left to right},
journal = {Information and {Control}},
year = 1965,
volume = 8,
pages = {607--639}
}
@InProceedings{luocall,
author = {Z. Luo and P. Callaghan},
title = {Mathematical Vernacular and Conceptual Well-Formedness in Mathematical
Language},
booktitle = {{Logical Aspects of Computational Linguistics (LACL)}} ,
year = 1999,
editor = {A. Lecomte and F. Lamarche and G. Perrier},
series = {{LNCS/LNAI}},
volume = 1582,
pages = {231--250}
}
@Book{hpsg,
author = "C. Pollard and I. Sag",
title = {{Head-Driven Phrase Structure Grammar}},
publisher = {{University of Chicago Press}},
year = 1994
}
@Book{lfg,
editor = "J. Bresnan",
title = {{The Mental Representation of Grammatical Relations}},
publisher = {{MIT Press}},
year = 1982
}
@ARTICLE{dcg,
AUTHOR = "F. Pereira and D. Warren",
TITLE = "Definite clause grammars
for language analysis---a survey of the formalism and a
comparison with augmented transition networks",
JOURNAL = {{Artificial Intelligence}},
VOLUME = {13},
PAGES = {231--278},
YEAR = {1980} }
@ARTICLE{mcfg,
author= {H. Seki and T. Matsumura and M. Fujii and T. Kasami},
title = "On Multiple Context-Free Grammars",
journal = {{Theoretical Computer Science}},
volume = 88,
pages = {191--229},
year = 1991
}
@inproceedings{cayenne,
AUTHOR = {L. Augustsson},
TITLE = {{Cayenne---a language with dependent types}},
BOOKTITLE = {Proc. of {ICFP'98}},
PUBLISHER = {ACM Press},
MONTH = {September},
YEAR = {1998}
}
@book{morrill,
AUTHOR = {G. Morrill},
TITLE = {{Type Logical Grammar}},
YEAR = {1994},
PUBLISHER = {Kluwer}
}
@book{nordstrom:book,
AUTHOR = {B. Nordstr{\"{o}}m and K. Petersson and J. M. Smith},
TITLE = {{Programming in Martin-Löf's Type Theory. An Introduction}},
YEAR = {1990},
PUBLISHER = {Oxford University Press}
}
@book{constable,
AUTHOR = {R. L. Constable},
TITLE = {{Implementing Mathematics with the NuPRL Proof Development System}},
YEAR = {1986},
PUBLISHER = {Prentice-Hall}
}
@book{martin-lof,
AUTHOR = {P. Martin-L\"{o}f},
TITLE = {{Intuitionistic Type Theory}},
ADDRESS = {Napoli},
YEAR = {1984},
PUBLISHER = {Bibliopolis}
}
@InProceedings{dymetman,
author = {M.\ Dymetman and V.\ Lux and A.\ Ranta},
title = {{XML} and Multilingual Document Authoring: Convergent Trends},
booktitle = {{COLING}, {Saarbr\"ucken}, {Germany}},
pages = {243--249},
year = {2000}
}
@InProceedings{GF-Alfa,
author = {T.\ Hallgren and A.\ Ranta},
title = {An Extensible Proof Text Editor},
editor = {M. Parigot and A. Voronkov},
booktitle = {{LPAR-2000}},
year = {2000},
series = {{LNCS/LNAI}},
volume = {1955},
publisher = {Springer},
pages = {70--84}
}
@InProceedings{FASE,
author = {R.\ Hähnle and K.\ Johannisson and A.\ Ranta},
title = {{An Authoring Tool for Informal and Formal Requirements Specifications}},
booktitle = {{Fundamental Approaches to Software Engineering}},
editor = {R.-D. Kutsche and H. Weber},
year = {2002},
series = {LNCS},
volume = {2306},
pages = {233--248},
publisher = {Springer}
}
@InProceedings{khegai,
author = {J.\ Khegai and B.\ Nordström and A.\ Ranta},
title = {{Multilingual Syntax Editing in GF}},
booktitle = {{Intelligent Text Processing and Computational Linguistics
(CICLing-2003), Mexico City, February 2003}},
year = {{2003}},
series = {LNCS},
volume = {2588},
editor = {A. Gelbukh},
pages = {453--464},
publisher = {Springer-Verlag}
}
@ARTICLE{gf-jfp,
AUTHOR = "A. Ranta",
TITLE = {{Grammatical Framework: A Type-theoretical Grammar Formalism}},
JOURNAL = {{The Journal of Functional Programming}},
pages={145--189},
volume={14(2)},
YEAR = {2004} }
@Misc{GF-homepage,
author = {A. Ranta},
title = {{Grammatical Framework Homepage}},
note = {\verb6www.cs.chalmers.se/~aarne/GF/6},
url = "http://www.cs.chalmers.se/~aarne/GF/",
year = 2002
}
@Misc{happy,
author = {S. Marlow},
title = {{Happy, The Parser Generator for Haskell}},
note = {\verb6http://www.haskell.org/happy/6},
year = 2001
}
@inproceedings{magnusson-nordstr,
AUTHOR = {L. Magnusson and B. Nordstr\"{o}m},
BOOKTITLE = {{Types for Proofs and Programs}},
PUBLISHER = {Springer},
SERIES = {LNCS 806},
PAGES = {213--237},
TITLE = {The {ALF} proof editor and its proof engine},
YEAR = {1994}
}
@Book{Ranta94,
author = {A. Ranta},
title = {{Type Theoretical Grammar}},
publisher = {Oxford University Press},
year = {1994}
}
@Misc{coq,
author = {{The Coq Development Team}},
title = {{The Coq Proof Assistant Reference Manual}},
howpublished = {\verb6pauillac.inria.fr/coq/6},
documentURL = "http://pauillac.inria.fr/coq/",
year = 1999
}
@InProceedings{wysiwym,
author = {R. Power and D. Scott},
title = {Multilingual authoring using feedback texts},
booktitle = {{COLING}-{ACL}},
year = 1998
}
@PhdThesis{fiedler,
author = {A. Fiedler},
title = {{User-Adaptive Proof Explanation}},
school = {{Universität des Saarlandes}},
year = 2001
}
@PhdThesis{peb,
author = {P. Ljungl\"of},
title = {{Grammatical Framework and Generalized Context-Free Grammars}},
school = {{Dept.\ of Computing Science,
Chalmers University of Technology and
Gothenburg University}},
year = {forthcoming}
}
@InProceedings{peb-parsing,
author = {P. Ljungl\"of},
title = {{Grammatical Framework and Multiple Context-Free Grammars}},
booktitle = {{Proceedings of Formal Grammar, Nancy, August 2004}},
editor = {G. Jaeger and P. Monachesi and G. Penn and S. Wintner},
pages = {77--90},
year = {2004}
}
@PhdThesis{fudgets,
author = {M. Carlsson and T. Hallgren},
title = {{Fudgets---Purely Functional Processes with
applications to Graphical User Interfaces}},
school = {{Department of Computing Science, Chalmers University
of Technology}},
year = 1998,
documentURL = "http://www.cs.chalmers.se/~hallgren/Thesis/"
}
@article{harper-honsell,
AUTHOR = {R. Harper and F. Honsell and G. Plotkin},
TITLE = {{A Framework for Defining Logics}},
JOURNAL = {{JACM}},
VOLUME = {40},
NUMBER = {1},
YEAR = {1993},
PAGES = {143--184}
}
@InProceedings{CKT95,
author = "Y. Coscoy and G. Kahn and L. Thery",
title = "Extracting text from proofs",
series = lncs,
volume = "902",
pages = {109--123},
year = "1995",
booktitle = "Proc.\ {Second} {Int.} {Conf.} on
{Typed} {Lambda} {Calculi} and {Applications}",
editor = "M. Dezani-Ciancaglini and G. Plotkin"
}
@Book{WarmerKleppe99,
author = "J. Warmer and A. Kleppe",
title = {{The Object Constraint Language: Precise Modelling with UML}},
publisher = {{Addison-Wesley}},
year = "1999"
}
@InProceedings{HoltEwan99,
author = {Alexander Holt and Ewan Klein},
title = {A semantically-derived subset of {E}nglish for
hardware verification},
booktitle = {Proc.\ Ann.\ Meeting Ass.\ for
Comp.\ Ling.},
pages = {451--456},
year = {1999},
url = {http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-sds/ps/}
}
@misc{bohlin-trindi,
author = {P. Bohlin and J. Bos and S. Larsson and
I. Lewin and C. Matheson and D. Milward},
year = 1999,
title = {Survey of Existing Interactive Systems},
note = {Trindi deliverable D1.3, Gothenburg University}
}
@Article{teitelbaum,
author = "T. Teitelbaum and T. Reps",
title = {The {Cornell} {Program} {Synthesizer}: a syntax-directed
programming environment},
journal = {Commun. {ACM}},
year = "1981",
volume = "24",
number = "9",
pages = {563-573}
}
@misc{haskell98,
author= {S. {Peyton Jones} and J. Hughes},
title={{Report on the Programming Language Haskell 98, a
Non-strict, Purely Functional Language}},
year=1999,
month={February},
howpublished={Available from \verb!http://www.haskell.org!}
}
@Manual{UML1.3-specification,
key = {UML 1.3},
title = {Unified Modelling Language Specification, version 1.3},
organization = {Object Modeling Group},
month = mar,
year = 2000,
url = {http://cgi.omg.org/cgi-bin/doc?formal/00-03-01.ps.gz},
note = {OMG document formal/00-03-01. {URL:}
\texttt{http://cgi.omg.org/cgi-bin/doc?formal/00-03-01.ps.gz}}
}
@TechReport{LBR00,
author = "G. T. Leavens and A. L. Baker and C. Ruby",
title = "Preliminary Design of {JML}: A Behavioral Interface
Specification Language for {Java}",
institution = "Iowa State University, Department of Computer
Science",
year = "2000",
number = "98-06i",
month = feb,
note = "URL: \texttt{ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz}",
url = "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz"
}
@TechReport{johnson-yacc,
author = {S. C. Johnson},
title = {{Yacc --- yet another compiler compiler}},
institution = {{AT \& T Bell Laboratories, Murray Hill, NJ}},
year = {1975},
number = {{CSTR-32}}
}
@TechReport{hallgren-2000,
author = {T. Hallgren},
title = {The Correctness of Insertion Sort},
institution = {Chalmers University of Technology,
Department of Computer Science},
year = {2000},
note = {URL: \verb!http://www.cs.chalmers.se/~hallgren/Papers/insertion_sort.ps!}
}
@InProceedings{power-scott-1998,
author = {R. Power and D. Scott},
title = {Multilingual authoring using feedback texts},
booktitle = {COLING-ACL 98},
year = 1998,
address = {Montreal, Canada}
}
@InProceedings{coquand1999,
author = {C. Coquand and T. Coquand},
title = {Structured Type Theory},
booktitle = {Workshop on Logical Frameworkds and Meta-languages},
year = 1999,
address = {Paris, France}
}
@book{mueller,
author = {Stefan Müller},
title = {{Deutsche Syntax Deklarativ}},
year = 1999,
publisher = {{Max Niemeyer Verlag}}
}
@article{ranta-cooper,
author = {A. Ranta and R. Cooper},
title = {{Dialogue Systems as Proof Editors}},
journal = {{Journal of Logic, Language and Information}},
year = 2004
}
@InProceedings{ranta-cooper-icos,
author = {A. Ranta and R. Cooper},
title = {Dialogue Systems as Proof Editors},
booktitle = {{IJCAR}/{ICoS-3}},
year = 2001,
address = {{Siena}, {Italy}}
}
@InProceedings{curry,
AUTHOR = "H. B. Curry",
TITLE = "Some logical aspects of grammatical structure",
EDITOR = "Jakobson, Roman",
BOOKTITLE = {{Structure of Language and its
Mathematical Aspects: Proceedings of the Twelfth Symposium
in Applied Mathematics}},
PUBLISHER = {American Mathematical Society},
YEAR = {1963},
PAGES = {56-68}
}
@inproceedings{bengt-lena1995,
AUTHOR = {L. Magnusson and B. Nordstr\"{o}m},
BOOKTITLE = {{ Types for Proofs and Programs}},
PUBLISHER = {Springer-Verlag},
SERIES = {LNCS},
VOL = {806},
PAGES = {213-237},
TITLE = {{The ALF proof editor and its proof engine}},
ADDRESS = {Nijmegen},
YEAR = {1994}
}
@article{kay1997,
AUTHOR = {M. Kay},
TITLE = {{The Proper Place of Men and Machines in Language Translation}},
JOURNAL = {{Machine Translation}},
YEAR = {1997},
NUMBER = {1--2},
VOLUME = {12},
PAGES = {3--23}
}
@unpublished{together,
title = {{Together}},
author = {{Borland Software Corporation}},
howpublished = {Online document},
year = {2004},
note = {\verb!http://www.borland.com/together/!}
}
@unpublished{lkb,
title = {{The LKB System}},
author = {Ann Copestake},
howpublished = {Online document},
year = {2002},
note = {Available on-line in \verb!http://www-csli.stanford.edu/~aac/lkb.html!}
}
@unpublished{eclipse,
title = {{Eclipse Homepage}},
author = {{Eclipse.org}},
howpublished = {Online document},
year = {2004},
note = {\verb!http://www.eclipse.org/!}
}
@unpublished{boeing,
title = {{Boeing Simplified English Checker}},
author = {{The Boeing Company}},
howpublished = {Online document},
year = {2001},
note = {\verb!http://www.boeing.com/assocproducts/sechecker/!}
}
@unpublished{XML,
title = {{Extensible Markup Language (XML)}},
author = {{The World Wide Web Consortium}},
howpublished = {Online document},
year = {2000},
note = {\verb!http://www.w3.org/XML/!}
}
@unpublished{huet-trie,
author = {G. Huet},
title = {{The Zen Computational Linguistics Toolkit}},
howpublished = {{ESSLLI Summer School, Trento}},
note = {\verb!http://pauillac.inria.fr/~huet/!},
year = 2002
}
@unpublished{agda-homepage,
author = "C. Coquand",
title = "{{AGDA Homepage}}",
year = 1998,
howpublished = {Online document},
note = {\verb!http://www.cs.chalmers.se/~catarina/agda/!} ,
documenturl = "http://www.cs.chalmers.se/~catarina/agda/"
}
@InProceedings{coquand:stt-lfm99,
author = {C. Coquand and T. Coquand},
title = {Structured Type Theory},
booktitle = {Workshop on Logical Frameworkds and Meta-languages},
year = 1999,
address = {Paris, France},
month = {Sep}
}
@inproceedings{augustsson:cayenne,
AUTHOR = {L. Augustsson},
TITLE = {{Cayenne --- a language with dependent types}},
BOOKTITLE = {Proc. of the International Conference on Functional Programming (ICFP'98)},
PUBLISHER = {ACM Press},
MONTH = {September},
YEAR = {1998}
}
@PhdThesis{carlsson98:fudgets_thesis,
author = {M. Carlsson and T. Hallgren},
title = {{Fudgets --- Purely Functional Processes with
applications to Graphical User Interfaces}},
booktitle = {{Fudgets --- Purely Functional Processes with
applications to Graphical User Interfaces}},
school = {Department of Computing Science, Chalmers University
of Technology},
year = 1998,
address = {S-412 96 Göteborg, Sweden},
month = {March},
documentURL = "http://www.cs.chalmers.se/~hallgren/Thesis/"
}
@book{martin-lof:padova,
AUTHOR = {P. Martin-L\"{o}f},
TITLE = {{Intuitionistic Type Theory}},
ADDRESS = {Napoli},
YEAR = {1984},
PUBLISHER = {Bibliopolis}
}
@book{montague,
AUTHOR = {R.\ Montague},
TITLE = {{Formal Philosophy}},
ADDRESS = {New Haven},
YEAR = {1974},
NOTE = {Collected papers edited by R.\ Thomason},
PUBLISHER = {Yale University Press}
}
@misc{alfa-homepage,
author = {T. Hallgren},
year = {2000},
title = {{Home Page of the Proof Editor Alfa}},
howpublished = {\verb!http://www.cs.chalmers.se/~hallgren/Alfa/!},
documentURL = {http://www.cs.chalmers.se/~hallgren/Alfa/}
}
@InProceedings{ranta98:regexp,
author = {A. Ranta},
title = {A Multilingual Natural-Language Interface to Regular Expressions},
booktitle = {Proceedings of the International Workshop on Finite State
Methods in Natural Language Processing},
pages = {79--90},
year = 1998,
editor = {L. Karttunen and K. Oflazer},
address = {Ankara},
organization = {Bilkent University}
}
@Misc{maple-homepage,
author = {Waterloo Maple Inc.},
title = {{Maple Homepage}},
howpublished = {\verb!http://www.maplesof.com/!},
documentURL = "http://www.maplesof.com/",
year = 2000
}
@Misc{mathematica-homepage,
author = {Wolfram Research, Inc.},
title = {{Mathematica Homepage}},
howpublished = {\verb!http://www.wolfram.com/products/mathematica/!},
documentURL = "http://www.wolfram.com/products/mathematica/",
year = 2000
}
@Misc{coq-homepage,
author = {Coq Development Team},
title = {{Coq Homepage}},
howpublished = {\verb!http://pauillac.inria.fr/coq/!},
documentURL = "http://pauillac.inria.fr/coq/",
year = 1999
}
@TechReport{LEGO-homepage,
author = {Z. Luo and R. Pollack},
title = {{LEGO Proof Development System}},
institution = {University of {Edinburgh}},
year = 1992
}
@Misc{LEGO-new-homepage,
author = {D. Aspinall},
title = {{The LEGO Proof Assistant}},
howpublished = {\verb!http://www.dcs.ed.ac.uk/home/lego/!},
documentURL = "http://www.dcs.ed.ac.uk/home/lego/",
year = 1999
}
@Misc{Isabelle-homepage,
author = {Isabelle},
title = {{Isabelle Homepage}},
howpublished = {\verb!http://www.cl.cam.ac.uk/Research/HVG/Isabelle/!},
documentURL = "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html",
year = 2000
}
@Misc{Isabelle-Paulson,
author = "L. Paulson",
title = {{The Isabelle Reference Manual}},
note = {{With contributions by T. Nipkow and M. Wenzel}},
howpublished = {Available at the Isabelle homepage \verb!http://www.cl.cam.ac.uk/Research/HVG/Isabelle/!},
documentURL = "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/Isabelle2002/doc/ref.pdf",
year = 2002
}
@Misc{Mizar-homepage,
author = {},
title = {{The Mizar Homepage}},
howpublished = {\verb!http://mizar.org/!},
documentURL = "http://mizar.org/",
year = 1999
}
@Misc{ALF-family-homepage,
author = {},
title = {{Implementation of Proof Editors}},
howpublished =
{\verb!http://www.cs.chalmers.se/ComputingScience/Research/Logic/!},
documentURL = "http://www.cs.chalmers.se/ComputingScience/Research/Logic/",
year = 1999
}
@incollection{deBruijn:MV,
TITLE = {{Mathematical Vernacular:
a Language for Mathematics with Typed Sets}},
AUTHOR = {N. G. de Bruijn},
EDITOR = {R. Nederpelt},
BOOKTITLE = {{Selected Papers on Automath}},
PUBLISHER = {{North-Holland Publishing Company}},
PAGES = {865--935},
YEAR = {1994}
}
@article{pereira-warren,
AUTHOR = "F. Pereira and D. Warren",
TITLE = "Definite Clause Grammars for Language Analysis",
JOURNAL = {Artificial {Intelligence}},
YEAR = {1980},
NUMBER = {13},
PAGES = {231--278}
}
@PhdThesis{coscoy:thesis,
author = {Y.\ Coscoy},
title = {Explication textuelle de preuves pour le calcul des
constructions inductives},
school = {{Universit\'e de Nice-Sophia-Antipolis}},
year = 2000
}
@InProceedings{coscoy:textproofs,
AUTHOR = {Y. Coscoy and G. Kahn and L. Th\'ery},
TITLE = {Extracting Text from Proof},
BOOKTITLE = {{Proceedings of the International Conference on Typed Lambda
Calculus and Applications (TLCA), Edinburgh}},
EDITOR = {M. Dezani and G. Plotkin},
SERIES = {Lecture Notes in Computer Science},
NUMBER = {902},
PUBLISHER = {Springer-Verlag},
YEAR = {1996}
}
@InProceedings{coscoy:explanation,
author = {Y. Coscoy},
title = {A natural language explanation of formal proofs},
booktitle = {Logical Aspects of Computational Linguistics},
pages = {149--167},
year = 1997,
editor = {C. {Retor\'e}},
address = {Heidelberg},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
number= 1328
}
@inproceedings{ranta:torino,
AUTHOR = {A. Ranta},
TITLE = {Context-Relative Syntactic Categories
and the Formalization of Mathematical Text},
BOOKTITLE = {{Types For Proofs and Programs}},
EDITOR = {S. Berardi and M. Coppo},
SERIES = {Lecture Notes in Computer Science},
NUMBER = {1158},
PAGES = {231--248},
PUBLISHER = {Springer-Verlag},
YEAR = {1996}
}
@article{ranta:paris,
AUTHOR = {A. Ranta},
TITLE = {{Structures grammaticales dans le fran\c{c}ais math\'ematique}},
JOURNAL = {{Math\'ematiques, informatique et Sciences Humaines}},
YEAR = {1997},
NUMBER = {138, 139},
PAGES = {5--56, 5--36}
}
@article{kamp:drt,
AUTHOR = {H. Kamp},
TITLE = {{ A theory of truth and semantic representation}},
EDITOR = {{J. Groenendijk, T. Janssen, and M. Stokhof}},
BOOKTITLE = {{Formal Methods in the Study of Language, Part 1}},
YEAR = {1981},
PUBLISHER = {{Mathematisch Centrum, Amsterdam}},
PAGES = {277--322}
}
@PhdThesis{magnusson:phd,
author = {L. Magnusson},
title = {The Implementation of ALF - a Proof Editor based on
Martin-L\"of's Monomorphic Type Theory with Explicit
Substitution},
school = {Department of Computing Science, Chalmers University of
Technology and University of G\"oteborg},
year = {1994}
}
@InProceedings{krijo-aarne,
author = "K. Johannisson and A. Ranta",
title = "Formal Verification of Multilingual Instructions",
booktitle = "The Joint Winter Meeting of Computing Science and
Computer Engineering",
publisher = "Chalmers University of Technology",
year = "2001"
}
@Manual{JavaCollection,
title = {The Java Collection Framework},
year = {1995--1999},
author = {{Sun Microsystems Inc.}},
note = {\texttt{http://java.sun.com/j2se/1.3/docs/guide/collections/}}
}
@Book{BarstowSandewall,
author = {Barstow, D.~R., Shrobe, H.~E., and Sandewall, E.},
title = {Interactive Programming Environments},
publisher = {McGraw Hill},
year = 1984
}
@inproceedings{HuetKahn1975,
author = "V. Donzeau-Gouge and G. Huet and G. Kahn and B. Lang and J.~J. Levy",
title = {A structure-oriented program editor:
a first step towards computer assisted programming},
booktitle = {{International Computing Symposium ({ICS'75})}},
year = {1975}
}
@Book{Sommerville01,
author = "Ian Sommerville",
title = "Software Engineering",
publisher = "Addison-Wesley",
year = "2001",
edition = "6th"
}
@InProceedings{HoltEwan99,
author = {Alexander Holt and Ewan Klein},
title = {A semantically-derived subset of {E}nglish for
hardware verification},
booktitle = {Proc.\ 37th Annual Meeting of the Association for
Computational Linguistics: Maryland, USA},
pages = {451-456},
year = {1999},
publisher = {Association for Computational Linguistics},
url = {\texttt{http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-sds/ps/}}
}
@InProceedings{HKG99,
author = {Alexander Holt and Ewan Klein and Claire Grover},
title = {Natural language for hardware verification:
semantic interpretation and model checking},
booktitle = {Proc.\ ICoS-1: Inference in Computational Semantics, Amsterdam},
pages = {133-137},
year = {1999},
publisher = {Institute for Logic, Language and Computation,
University of Amsterdam},
url = {http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-nlh/ps/}
}
@Article{Holt99,
author = {Alexander Holt},
title = {Formal verification with natural language specifications:
guidelines, experiments and lessons so far},
journal = {South African Computer Journal},
year = {1999},
volume = {24},
pages = {253-257},
month = nov,
url = {http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-fvn/ps/},
}
@InProceedings{HaehnleRanta01a,
author = {R.\ H\"{a}hnle and A.\ Ranta},
title = {Connecting {OCL} with the Rest of the World},
booktitle = {{ETAPS}/{WTUML},
{Genova}, {Italy}},
year = {2001},
editor = {J. Whittle},
url = {http://www.cs.chalmers.se/~reiner/papers/wtuml.ps.gz}
}
@Article{BBEHO99,
author = "Michael Baentsch and Peter Buhler and Thomas Eirich
and Frank H{\"o}ring and Marcus Oestreicher",
title = "{JavaCard} --- From Hype to Reality",
journal = "IEEE Concurrency",
volume = "7",
number = "4",
pages = "36--43",
month = oct # "\slash " # dec,
year = "1999",
url = "http://www.zurich.ibm.com/technologies/jetz/p4baenCPYRT.lo.pdf"
}
@InProceedings{GogollaRichters98a,
author = "Martin Gogolla and Mark Richters",
title = "On Constraints and Queries in {UML}",
pages = "109--121",
booktitle = "The Unified Modeling Language -- Technical Aspects and
Applications",
editor = "Martin Schader and Axel Korthaus",
publisher = "Physica-Verlag, Heidelberg",
year = "1998"
}
@InProceedings{HHK98,
author = "Ali Hamie and John Howse and Stuart Kent",
title = "Interpreting the {Object Constraint Language}",
booktitle = "Proceedings 5th Asia Pacific Software Engineering
Conference (APSEC '98), Taipei,
Taiwan",
year = "1998",
publisher = "IEEE Computer Society"
}
@Book{HKT00,
author = {David Harel and Dexter Kozen and Jerzy Tiuryn},
title = {Dynamic Logic},
publisher = {MIT Press},
year = 2000,
series = {Foundations of Computing},
month = oct,
isbn_issn = {0-262-08289-6}
}
@Book{MichalewiczFogel00,
author = {Z. Michalewicz and B. F. Fogel},
title = {How to solve it: modern heuristics},
publisher = spv,
year = {2000},
isbn_issn = {3-540-66061-5}
}
@Book{Schumann00,
author = {Johann M. P. Schumann},
title = {Automated Theorem Proving in Software Engineering},
publisher = spv,
year = {2000},
isbn_issn = {3-540-67989-8}
}
@Book{HMNS00,
author = {U. Hansmann and L. Merk and M. S. Nicklous and T. Stober},
title = {Pervasive Computing Handbook},
publisher = spv,
year = {2000},
isbn_issn = {3-540-67122-6}
}
@Book{Newborn00,
author = {M. Newborn},
title = {Automated Theorem Proving: Theory and Practice},
publisher = spv,
year = {2000},
isbn_issn = {3-387-95075-3}
}
@Book{TymoczkoHenle00,
author = {T. Tymoczko and J. Henle},
title = {Sweet Reason: A Field Guide to Modern Logic},
publisher = spv,
year = {2000},
isbn_issn = {3-387-98930-7}
}
@Book{HMT99,
editor = {Hatcliff, J. and Mogensen, T. and Thiemann, P.},
title = {Partial Evaluation. Practice and Theory.
DIKU 1998 International Summer School, Copenhagen, Denmark},
publisher = spv,
year = {1999},
volume = {1706},
series = lncs,
isbn_issn = {3-540-66710-5}
}
@inproceedings{Giese00,
author = {Martin Giese},
title = {Proof Search without Backtracking using Instance Streams, Position Paper},
booktitle = {Proc.\ Int.\ Workshop on First-Order Theorem Proving, St.\ Andrews, Scotland},
year = {2000},
pages = {227--228},
editor = {Peter Baumgartner and Hantao Zhang},
series = {Fachberichte Informatik 5/2000},
publisher = {University of Koblenz, Institute for Computer Science},
note = {\href{http://i12www.ira.uka.de/~key/doc/2000/giese00.ps.gz}{\texttt{http://i12www.ira.uka.de/\~{}key/doc/2000/giese00.ps.gz}}}
}
@article{Smullyan63,
AUTHOR = {Smullyan, Raymond M.},
TITLE = {A unifying principle in quantification theory},
JOURNAL = {Proceedings of the National Academy of Sciences of the U.S.A.},
VOLUME = {49},
number = {6},
YEAR = {1963},
PAGES = {828--832}
}
@InProceedings{BaarHaehnle00a,
author = {Thomas Baar and Reiner H\"ahnle},
title = {An Integrated Metamodel for {OCL} Types},
booktitle = {Proc.\ OOPSLA 2000 Workshop Refactoring the UML:
In Search of the Core, Minneapolis/MI, USA},
year = {2000},
editor = {Robert France and Bernhard Rumpe and Jonathan Whittle},
month = oct
}
@InCollection{RSBMZ98,
author = {Dirk Riehle and Wolf Siberski and Dirk B\"{a}umer and
Daniel Megert and Heinz Z\"{u}llighoven.},
title = {Serializer},
booktitle = {Pattern Languages of Program Design 3},
pages = {293--312},
publisher = {Addison-Wesley},
year = {1998},
editor = {Robert Martin and Dirk Riehle and and Frank Buschmann},
chapter = {17},
url = {http://www.riehle.org/papers/1996/plop-1996-serializer.pdf}
}
@InProceedings{CIOH00,
author = {Cristiano Calcagno and Samin Ishtiaq and Peter W. O'Hearn},
title = {Semantic Analysis of Pointer Aliasing, Allocation and
Disposal in {H}oare Logic},
booktitle = {Proc.\ 2nd International Conference on Principles
and Practice of Declarative Programming, Montral, Canada},
year = {2000},
editor = {Maurizio Gabbrielli and Frank Pfenning},
series = lncs,
publisher = spv,
url = {http://www.dcs.qmw.ac.uk/~ccris/ftp/ppdp00.ps}
}
@Book{PalanquePaterno98,
editor = {P. Palanque and F. Patern\`{o}},
title = {{Formal Methods in Human-Computer Interaction}},
publisher = spv,
series = {{FACIT}},
year = {{1998}}
}
@Book{VanDerLinden99a,
author = "Peter {van der Linden}",
title = "Just {Java} 1.2",
publisher = "Prentice-Hall",
edition = "Fourth",
month = mar,
year = "1999",
ISBN_ISSN = "0-13-010534-1",
series = "SunSoft Press Java series"
}
@Book{VanDerLinden99b,
author = "Peter {van der Linden}",
title = "Not Just {Java}: a technology briefing",
publisher = "Prentice-Hall",
edition = "Second",
year = "1999",
ISBN_ISSN = "0-13-079660-3",
series = "SunSoft Press Java series"
}
Book{GoldbergRubin95,
author = "Adele Goldberg and Kenneth S. Rubin",
title = "Succeeding With Objects: Decision Frameworks for
Project Management",
publisher = "Addison-Wesley",
year = "1995",
ISBN_ISSN = "0-201-62878-3"
}
@Book{Goldberg84,
author = "Adele Goldberg",
title = "Smalltalk-80: the Interactive Programming
Environment",
publisher = "Addison-Wesley",
year = "1984",
ISBN_ISSN = "0-201-11372-4"
}
@Book{GoldbergRobson83,
author = "Adele Goldberg and David Robson",
title = "Smalltalk-80: The Language and its Implementation",
publisher = "Addison-Wesley",
year = "1983"
}
@Book{Ranta01a,
author = {Sara Negri and Jan von Plato},
title = {Structural Proof Theory},
publisher = {Cambridge University Press},
year = {2001, to appear},
note = {Appendix C ``PESCA---A Proof Editor for Sequent Calculus''
by Aarne Ranta}
}
@Manual{Ranta00a,
title = {PESCA---A Proof Editor for Sequent Calculus},
author = {Aarne Ranta},
organization = {Department of Computing Science,
Chalmers University of Technology and University of Gothenburg},
address = {Gothenburg},
month = mar,
year = {2000},
note = {Program and documentation.
URL: \texttt{www.cs.chalmers.se\~{}aarne/pesca/}}
}
@InProceedings{MaenpaaRanta99,
author = {P. Mäenpää and A. Ranta},
title = {The type theory and type checker of {GF}},
booktitle = {{PLI-1999:
Workshop on Logical Frameworks and Meta-languages,
Paris, France}},
year = {1999}
}
@Article{Ranta88,
author = "Aarne Ranta",
title = {Propositions as games as types},
journal = {Synthese},
year = {1988},
volume = {76},
pages = {377--395}
}
@Article{Ranta91b,
author = "Aarne Ranta",
title = {Intuitionistic categorial grammar},
journal = {Linguistics and Philosophy},
year = {1991},
volume = {14},
pages = {203--239}
}
@Article{Ranta95c,
author = "Aarne Ranta",
title = {Type-theoretical interpretation and generalization
of phrase structure grammar},
journal = {{Bulletin of the IGPL}},
year = {1995},
volume = {3},
pages = {319--342}
}
@Article{Ranta97a,
author = "Aarne Ranta",
title = {Structures grammaticales dans le fran\c{c}ais math\'{e}matique},
journal = {Math\'{e}matiques, informatique et Sciences Humaines},
year = {1997},
volume = {138/139},
pages = {5--56/5--36}
}
@InProceedings{Ranta94a,
author = "Aarne Ranta",
title = "Type Theory and the Informal Language of Mathematics",
booktitle = "Selected papers from TYPES'93:
Int.\ Workshop on Types, Nijmegen, The Netherlands",
series = lncs,
publisher = spv,
volume = "806",
pages = "352--365",
year = "1994",
editor = "Hendrik Barendregt and Tobias Nipkow"
}
@InProceedings{Ranta96a,
author = "A. Ranta",
title = "Context-Relative Syntactic Categories and the
Formalization of Mathematical Text",
booktitle = "Selected papers from TYPES'95: Int.\ Workshop on Types for
Proofs and Programs, Trento, Italy",
publisher = spv,
editor = "S. Berardi and M. Coppo",
series = lncs,
volume = 1158,
pages = "231--248",
year = "1996"
}
@InProceedings{Ranta95a,
author = "Aarne Ranta",
title = "Syntactic Categories in the Language of Mathematics",
series = lncs,
volume = "996",
pages = "162--182",
year = "1995",
publisher = spv,
booktitle = "Selected papers from TYPES'94:
Int.\ Workshop on Types for
Proofs and Programs, Bastad, Sweden",
editor = {Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith}
}
@Article{Ranta98a,
author = "Aarne Ranta",
title = "Syntactic Calculus with Dependent Types",
journal = "Journal of Logic, Language, and Information",
year = "1998",
volume = "7",
number = "4",
pages = "413--431"
}
@InCollection{Ranta98b,
author = "Aarne Ranta",
title = "A Multilingual Natural Language Interface to Regular
Expressions",
booktitle = "{FSMNLP'98}: International Workshop on Finite State
Methods in Natural Language Processing",
publisher = "Bilkent University, Ankara",
year = "1998",
editor = "Lauri Karttunen and K. Oflazer",
pages = "79--90"
}
@Article{Ranta91a,
author = "Aarne Ranta",
title = "Constructing Possible Worlds",
journal = "Theoria",
volume = "57",
number = "1--2",
pages = "77--100",
year = "1991"
}
@InProceedings{semBNF,
author = {{P. M\"aenp\"a\"a}},
title = {{Semantic BNF}},
booktitle = "Types for Proofs and Programs, TYPES'96",
series = lncs,
publisher = spv,
volume = "1512",
pages = "196--215",
year = "1998",
editor = "E. Gimenez and C. Paulin-Mohring"
}
@MastersThesis{Schneider97,
author = {J\"{o}rg Schneider},
title = "{Formale Spezifikation eines
Autorisierungskonzepts am Beispiel des
Berechtigungswesens im SAP R/3-System}",
school = "Department of Computer Science, University of Karlsruhe",
year = "1997",
type = {Diplomarbeit}
}
@InProceedings{MandelCengarle99,
author = "Luis Mandel and Mar{\'\i}a Victoria Cengarle",
title = "On the Expressive Power of {OCL}",
booktitle = "Proc.\ FM'99 -- Formal Methods, World Congress on Formal
Methods in the Development of Computing Systems,
Toulouse, France",
year = "1999",
volume = "1708",
series = lncs,
pages = "854--874",
publisher = spv
}
@INCOLLECTION{steedman,
AUTHOR = "M. Steedman",
TITLE = "Combinators and grammars",
EDITOR = "R. Oehrle and E. Bach and D. Wheeler",
BOOKTITLE = {{Categorial Grammars and Natural Language Structures}},
PUBLISHER = {D. Reidel},
ADDRESS = {Dordrecht},
YEAR = {1988},
PAGES = {417-442}}
@InProceedings{DLR00,
author = {M.\ Dymetman and V.\ Lux and A.\ Ranta},
title = {{XML} and Multilingual Document Authoring: Convergent Trends},
booktitle = {Proc.\ Computational Linguistics COLING, Saarbr\"{u}cken, Germany},
pages = {243-249},
year = {2000},
publisher = {International Committee on Computational Linguistics}
}
@InProceedings{HallgrenRanta000,
author = {T. Hallgren and A. Ranta},
title = {Grammatical Annotations: a Method of Program Documentation},
booktitle = {Proc.\ International Conference on Functional Programming ICFP},
year = {submitted, 2000},
note = {URL: \texttt{http://www.cs.chalmers.se/\~{}aarne/hallgren-ranta-2000.ps.gz}}
}
@inproceedings{ mccarthy62towards,
author = "J.\ McCarthy",
title = "Towards a mathematical science of computation",
booktitle = "Proceedings of the Information Processing Cong. 62",
month = "August",
publisher = "North-Holland",
address = "Munich, West Germany",
pages = "21--28",
year = "1962"
}
@InProceedings{hallgren-ranta:lpar2000,
author = {T.\ Hallgren and A.\ Ranta},
title = {An Extensible Proof Text Editor},
editor = {M. Parigot \& A. Voronkov},
booktitle = {Logic for Programming and Automated Reasoning (LPAR'2000)},
year = {2000},
series = {LNCS/LNAI 1955},
pages = {70--84}
}
@InProceedings{DahnWolf96,
author = "Bernd I. Dahn and Andreas Wolf",
title = "Natural Language Representation and Combination of
Automatically Generated Proofs",
editor = "Franz Baader and Klaus U.~Schulz",
booktitle = "Frontiers of Combining Systems: Proc.\ 1st
International Workshop, Munich, Germany",
publisher = "Kluwer Academic Publishers",
series = "Applied Logic",
month = mar,
year = "1996",
pages = "175--192"
}
@Manual{Ranta99,
title = {Grammatical Framework Homepage},
author = {Aarne Ranta},
organization = {Chalmers University of Technology},
address = {Gothenburg},
year = {2001},
note = {URL: \texttt{www.cs.chalmers.se/~aarne/GF}}
}
@Manual{Ranta99a,
title = {Grammatical Framework Syntax and Semantic},
author = {Aarne Ranta},
organization = {Xerox Research Centre Europe},
address = {Grenoble},
month = feb,
year = {1999},
note = {URL: \texttt{www.xrce.xerox.com/research/mltt/gf/doc/gf-language/index.html}}
}
@Manual{Ranta99c,
title = {Grammatical Framework Implementation and Interfaces.
{R}evised for {GF} Version 0.5},
author = {Aarne Ranta},
organization = {Department of Computing Science,
Chalmers University of Technology},
month = jun,
year = {1999},
note = {URL: \texttt{www.cs.chalmers.se/\~{}aarne/GF/pub/doc/gf-implementation/index.html}}}
@Manual{Ranta99b,
title = {Grammatical Framework Tutorial},
author = {A. Ranta},
organization = {Xerox Research Centre Europe},
address = {Grenoble},
month = feb,
year = 1999,
note = {URL: \texttt{www.xrce.xerox.com/research/mltt/gf/doc/gf-tutorial/index.html}}
}
@TechReport{KeY00,
author = {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert
and Martin Giese and Elmar Habermalz and Reiner
H\"ahnle and Wolfram Menzel and Peter H. Schmitt},
title = {The {KeY} Approach: {I}ntegrating Object Oriented
Design and Formal Verification},
institution = {University of Karlsruhe, Department of Computer Science},
type = {Technical Report},
number = {2000/4},
month = jan,
year = {2000},
note = {URL: \texttt{i12www.ira.uka.de/\~{}key/doc/2000/techRep.ps.gz}}
}
@InProceedings{KeY00a,
author = {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert
and Martin Giese and Elmar Habermalz and Reiner
H\"ahnle and Wolfram Menzel and Peter H. Schmitt},
booktitle = {In Proc.\ Java Card Workshop, Cannes, France},
title = {The {KeY} Approach: {I}ntegrating Object Oriented
Design and Formal Verification},
month = sep,
year = {2000},
publisher = {{INRIA} technical report}
}
@article{Hughes89,
AUTHOR = {John Hughes},
TITLE = {Why Functional Programming Matters},
JOURNAL = {Computer Journal},
VOLUME = {32},
NUMBER = {2},
PAGES = {98--107},
YEAR = {1989}
}
@Book{RussellNorvig95,
author = "Stuart J. Russell and Peter Norvig",
title = "Artificial Intelligence. {A} Modern Approach",
publisher = "Prentice-Hall",
address = "Englewood Cliffs",
year = "1995",
url = "http://www.cs.berkeley.edu/~russell/aima.html"
}
@inproceedings{Thompson97a,
author = {Simon Thompson},
title = {{\em Where do I begin?}
{A} problem solving approach to teaching
functional programming},
month = sep,
year = {1997},
pages = {},
url = {http://www.cs.ukc.ac.uk/pubs/1997/208},
booktitle = {First International Conference on Declarative Programming Languages in Education},
editor = {Krzysztof Apt and Pieter Hartel and Paul Klint},
publisher = spv,
volume = "1292",
pages = "323--337",
series = lncs
}
@InProceedings{DAC98a,
author = "Matthew B. Dwyer and George S. Avrunin and James C.
Corbett",
title = "Property Specification Patterns for Finite-State
Verification",
pages = "7--15",
ISBN_ISSN = "0-89791-954-8",
editor = "Mark Ardis",
booktitle = "Proc.\ 2nd Workshop on Formal Methods in
Software Practice ({FMSP}-98)",
month = mar,
publisher = "ACM Press",
address = "New York",
year = "1998"
}
@InProceedings{DAC99a,
author = "Matthew B. Dwyer and George S. Avrunin and James C.
Corbett",
title = "Patterns in Property Specifications for Finite-State
Verification",
booktitle = "Proc.\ 21st International Conference on
Software Engineering",
year = "1999",
publisher = "IEEE Computer Society Press, ACM Press",
ISBN_ISSN = "1-58113-074-0",
pages = "411--420"
}
@Article{Fitting98a,
author = "Fitting",
title = "lean{TAP} Revisited",
journal = "jlc",
volume = "8",
number = "1",
pages = "33--47",
year = "1998"
}
@TechReport{NeculaLee96,
author = "G. C. Necula and P. Lee",
title = "Proof-Carrying Code",
institution = "School of Computer Science, Carnegie Mellon
University, Pittsburgh, USA",
year = "1996",
number = "CMU-CS-96-165",
month = nov,
url = "http://www.cs.cmu.edu/~necula/tr96-165.ps.gz"
}
@InProceedings{NeculaLee98,
author = "George C. Necula and Peter Lee",
title = "Safe, Untrusted Agents using Proof-Carrying Code",
booktitle = "Mobile Agents and Security",
volume = "1419",
year = "1998",
publisher = spv,
series = lncs,
editor = "Giovanni Vigna",
pages = "61--91",
url = "http://www.cs.cmu.edu/~necula/lncs98.ps.gz",
ISBN_ISSN = "0302-9743"
}
@InProceedings{Necula97,
author = "G. C. Necula",
title = {{Proof-Carrying Code}},
booktitle = {{Proc.\ 24th {A}{C}{M} Symposium on Principles of
Programming Languages, {Paris}, {France}}},
year = "1997",
url = "http://www.cs.cmu.edu/~necula/popl97.ps.gz",
pages = "106--119",
publisher = "ACM Press"
}
@Article{patr,
author = {L. Karttunen},
title = {PATR},
journal = ???,
year = 1981,
volume = 0,
pages = 0
}
@Misc{hallgren-sort,
author = "T. Hallgren",
title = "The correctness of insertion sort",
howpublished = www,
documentURL = cs.chalmers,
year = 2000
}
@Article{discont,
author = "H. Uszkoreit",
title = "German word order",
journal = ???,
year = 1988,
volume = ???,
pages = ???
}
@Article{hoas,
author = "J. Despeyroux",
title = "Higher-Order Abstract Syntax",
journal = ???,
year = 1995,
volume = ???,
pages = ???
}
@inproceedings{airline,
AUTHOR = {L. Augustsson},
TITLE = {{Partial Evaluation in Airline Crew Scheduling}},
BOOKTITLE = {???},
PUBLISHER = {???},
YEAR = {???}
}
Reference in New Issue View Git Blame Copy Permalink