biblio-gen.bib
@BOOK{Allen78,
AUTHOR = {John Allen},
TITLE = {{Anatomy of Lisp}},
PUBLISHER = {McGraw-Hill Book Compagny},
YEAR = 1978
}
@TECHREPORT{Barendregt91,
AUTHOR = {H. Barendregt},
INSTITUTION = {Catholic University Nijmegen},
NOTE = {in Handbook of Logic in Computer Science, Vol II},
NUMBER = {91-19},
TITLE = {{Lambda Calculi with Types}},
TYPE = {Technical Report},
YEAR = {1991}
}
@INCOLLECTION{Barendregt91b,
AUTHOR = {H. Barendregt},
TITLE = {Lambda Calculi With Types},
BOOKTITLE = {{Handbook of Logic in Computer Science}},
PUBLISHER = {Oxford University Press},
EDITOR = {Samson Abramsky and Dov Gabbay and Tom S.E. Maibaum},
CHAPTER = {2.2},
YEAR = {1992}
}
@MISC{ObjectiveCaml,
TITLE = {{The Objective Caml language}},
NOTE = {\url{http://pauillac.inria.fr/ocaml/}}
}
@MISC{Camlp4,
AUTHOR = {Daniel de Rauglaudre},
TITLE = {{The Camlp4 Pre Processor}},
NOTE = {\url{http://caml.inria.fr/camlp4/}}
}
@MANUAL{ObjectiveCamlManual,
TITLE = {The Objective Caml system:
Documentation and user's manual},
AUTHOR = {X. Leroy},
YEAR = 1997,
MONTH = {March},
NOTE = {\url{http://pauillac.inria.fr/ocaml/htmlman/}}
}
@PHDTHESIS{Castagna,
AUTHOR = {G. Castagna},
TITLE = {Surcharge, sous-typage et liaison tardive~: fondements
fonctionnels de la programmation orient\'ee objet},
SCHOOL = {Universit\'e Paris VII},
YEAR = {1994},
MONTH = {Janvier},
TYPE = {Th\`ese de doctorat}
}
@MISC{CoqProofAssistant,
AUTHOR = {Coq},
TITLE = {{The Coq Proof Assistant}},
YEAR = 2001,
NOTE = {\url{http://coq.inria.fr/}}
}
@MANUAL{CoqTutorial61,
TITLE = {The {C}oq {P}roof {A}ssistant {V}ersion 6.1, {A} {T}utorial},
AUTHOR = {G. Huet and G. Kahn and C. Paulin-Mohring},
YEAR = 1996,
MONTH = {December}
}
@INPROCEEDINGS{CoquandHuet85,
AUTHOR = {T. Coquand and G. Huet},
ADDRESS = {Linz},
BOOKTITLE = {{EUROCAL'85}},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 203,
PUBLISHER = {Springer-Verlag},
TITLE = {{Constructions: A Higher Order Proof System for Mechanizing Mathematics}},
YEAR = {1985}
}
@ARTICLE{CoquandHuet86,
AUTHOR = {T. Coquand and G. Huet},
JOURNAL = {Information and Computation},
NUMBER = {2/3},
TITLE = {The {Calculus of Constructions}},
VOLUME = {76},
PAGES = {95--120},
YEAR = {1988}
}
@UNPUBLISHED{Coquand86,
AUTHOR = {T. Coquand},
TITLE = {Metamathematical {I}nvestigations of a {C}alculus of
{C}onstructions},
NOTE = {INRIA and Cambridge University},
YEAR = 1986
}
@ARTICLE{Church32,
AUTHOR = {A. Church},
TITLE = {A set of postulates for the foundation of logic},
JOURNAL = {Annals of Mathematics},
YEAR = {1932/33},
VOLUME = {2},
NUMBER = {33-34},
PAGES = {346--366 and 839--864}
}
@ARTICLE{Church40,
AUTHOR = {A. Church},
TITLE = {A formulation of the simple theory of types},
JOURNAL = {Journal of Symbolic Logic},
YEAR = {1940},
VOLUME = {5},
PAGES = {56--68}
}
@BOOK{Church41,
AUTHOR = {A. Church},
TITLE = {The Calculi of Lambda Conversion},
PUBLISHER = {Princeton University Press},
YEAR = {1941}
}
@INPROCEEDINGS{Goubault93,
AUTHOR = {Jean Goubault},
TITLE = {{Implementing Functional Languages with Fast Equality,
Sets and Maps: an Exercise in Hash Consing}},
BOOKTITLE = {{Journ\'ees Francophones des Langages Applicatifs (JFLA'93)}},
PAGES = {222--238},
YEAR = 1993,
ADDRESS = {Annecy},
MONTH = {February},
URL = {http://www.dyade.fr/en/actions/vip/jgl/sharing.ps.gz}
}
@INCOLLECTION{Gentzen69,
AUTHOR = {G. Gentzen},
TITLE = {Investigations into logical deduction},
BOOKTITLE = {{The collected papers of Gerhard Gentzen}},
EDITOR = {M. E. Szabo},
PUBLISHER = {North Holland},
YEAR = {1969}
}
@PHDTHESIS{Geuvers93,
AUTHOR = {H. Geuvers},
TITLE = {Logics and Type Systems},
SCHOOL = {Catholic University Nijmegen},
MONTH = {September},
YEAR = {1993}
}
@INPROCEEDINGS{Gimenez94,
AUTHOR = {E. Gim\'enez},
TITLE = {{Codifying guarded definitions with recursive schemes}},
BOOKTITLE = {{Workshop on Types for Proofs and Programs}},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 996,
YEAR = 1994,
PAGES = {39--59}
}
@UNPUBLISHED{Gimenez95,
AUTHOR = {E. Gim\'enez},
TITLE = {{An Application of Co-Inductive Types in Coq:
Verification of the Alternating Bit Protocol}},
BOOKTITLE = {{Workshop on Types for Proofs and Programs}},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1158,
PAGES = {135--152},
YEAR = {1995},
PS = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR95/RR95-38.ps.Z}
}
@PHDTHESIS{Girard72,
AUTHOR = {J.-Y. Girard},
SCHOOL = {Univerit\'e Paris~7},
TITLE = {Interpr\'etation fonctionnelle et \'elimination des
coupures de l'arithm\'etique d'ordre sup\'erieur},
YEAR = 1972,
TYPE = {Th\`ese de doctorat d'\'{E}tat}
}
@BOOK{Harrison78,
AUTHOR = {M. A. Harrison},
TITLE = {Introduction to Formal Language Theory},
PUBLISHER = {Addison-Wesley},
YEAR = {1978}
}
@BOOK{HopcroftUllman79,
AUTHOR = {J. E. Hopcroft and J. D. Ullman},
TITLE = {{Introduction to Automata Theory, Languages, and Computation}},
PUBLISHER = {Addison-Wesley},
YEAR = {1979}
}
@INCOLLECTION{Howard80,
AUTHOR = {W. A. Howard},
TITLE = {The formulae-as-types notion of construction},
BOOKTITLE = {{To H. B. Curry: Essays on Combinatory Logic,
Lambda-Calculus and Formalism}},
PUBLISHER = {Academic Press},
EDITOR = {Hindley and Seldin},
YEAR = {1980},
PAGES = {479--490}
}
@INPROCEEDINGS{HuetSaibi95,
TITLE = {Constructive Category Theory},
AUTHOR = {G. Huet and A. Sa\"\i bi},
YEAR = {1995},
MONTH = {January},
NOTE = {in CLICS-TYPES BRA meeting}
}
@UNPUBLISHED{HuetSaibi96,
AUTHOR = {G.~Huet and A.~Sa\"{\i}bi},
TITLE = {Constructive Category Theory},
NOTE = {To appear},
YEAR = 1996
}
@MANUAL{Jones95,
TITLE = {An introduction to {G}ofer},
AUTHOR = {M. P. Jones},
YEAR = 1995,
MONTH = {June},
NOTE = {Draft version}
}
@ARTICLE{KleeneRosser35,
AUTHOR = {S. C. Kleene and J. B. Rosser},
TITLE = {The inconsistency of certain formal logics},
JOURNAL = {Annals of Mathematics},
YEAR = {1935},
VOLUME = {2},
NUMBER = {36},
PAGES = {630--636}
}
@TECHREPORT{Kreitz86,
AUTHOR = {C. Kreitz},
TITLE = {Constructive {A}utomata {T}heory {I}mplemented with the
{N}uprl {P}roof {D}evelopment {S}ystem},
INSTITUTION = {Cornell University, Department of Computer Science},
YEAR = 1986,
NUMBER = {TR 86--779},
MONTH = {September}
}
@MANUAL{Melham92,
TITLE = {The HOL {\tt finite\_sets} Library},
AUTHOR = {T. F. Melham},
ORGANIZATION = {University of Cambridge, Computer Laboratory},
YEAR = 1992,
MONTH = {February}
}
@BOOK{Nuprl86,
AUTHOR = {R.L. {Constable et al.}},
TITLE = {Implementing Mathematics with the Nuprl Proof Development
System},
PUBLISHER = {Prentice Hall},
YEAR = {1986}
}
@INPROCEEDINGS{OkasakiGill98,
AUTHOR = {Chris Okasaki and Andrew Gill},
TITLE = {{Fast Mergeable Integer Maps}},
BOOKTITLE = {{Workshop on ML}},
PAGES = {77--86},
YEAR = 1998,
MONTH = {September},
URL = {http://www.cs.columbia.edu/~cdo/ml98maps.ps.gz}
}
@ARTICLE{Omega,
AUTHOR = {William Pugh},
TITLE = {{The Omega Test: a fast and practical integer programming
algorithm for dependence analysis}},
JOURNAL = {Communications of the ACM},
VOLUME = 35,
NUMBER = 8,
PAGES = {102--114},
YEAR = 1992,
MONTH = {August}
}
@TECHREPORT{Parent93,
AUTHOR = {C. Parent},
INSTITUTION = {{\'Ecole Normale Sup\'erieure de Lyon}},
MONTH = OCT,
NUMBER = {93-29},
TITLE = {Developing certified programs in the system
{{Coq}} -- {The} {Program} tactic},
YEAR = 1993,
NOTE = {Also in \textit{Proceedings of the BRA
Workshop Types for Proofs and Programs}, May 93}
}
@PHDTHESIS{Parent95,
AUTHOR = {C. Parent},
TITLE = {Synth\`ese de preuves de programmes dans le {C}alcul
des {C}onstructions {I}nductives},
SCHOOL = {{\'Ecole Normale Sup\'erieure de Lyon}},
YEAR = 1995,
MONTH = {Janvier},
TYPE = {Th\`ese de doctorat}
}
@INPROCEEDINGS{Paulin89a,
AUTHOR = {C. Paulin-Mohring},
TITLE = {Extracting ${F}_{\omega}$'s programs from proofs in the
{C}alculus of {C}onstructions},
YEAR = 1989,
BOOKTITLE = {{Sixteenth Annual ACM Symposium on Principles of
Programming Languages}},
PUBLISHER = {ACM},
ADDRESS = {Austin},
MONTH = {January}
}
@PHDTHESIS{Paulin89b,
AUTHOR = {C. Paulin-Mohring},
TITLE = {{Extraction de programmes dans le Calcul des
Constructions}},
SCHOOL = {Universit\'e de Paris VII},
MONTH = {Janvier},
YEAR = {1989},
TYPE = {Th\`ese de doctorat}
}
@TECHREPORT{Paulin93a,
AUTHOR = {C. Paulin-Mohring},
TITLE = {Inductive Definitions in the system {\sf Coq}},
INSTITUTION = {LIP - ENS Lyon},
YEAR = {1993},
NUMBER = {92-49}
}
@INPROCEEDINGS{Paulin93,
AUTHOR = {C. Paulin-Mohring},
BOOKTITLE = {{Proceedings of the conference Typed Lambda Calculi and Applications}},
EDITOR = {M. Bezem and J.-F. Groote},
INSTITUTION = {LIP-ENS Lyon},
NOTE = {Also LIP research report 92-49},
VOLUME = {664},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
TITLE = {{Inductive Definitions in the System {Coq} - Rules and Properties}},
TYPE = {research report},
YEAR = {1993}
}
@ARTICLE{PaulinWerner92,
AUTHOR = {C. Paulin-Mohring and B. Werner},
JOURNAL = {Journal of Symbolic Computation},
TITLE = {{Synthesis of ML programs in the system Coq}},
VOLUME = {15},
YEAR = {1993},
PAGES = {607--640}
}
@ARTICLE{Plotkin75,
AUTHOR = {Gordon D. Plotkin},
TITLE = {{Call-by-Name, Call-by-Value and the lambda-Calculus}},
JOURNAL = {Theoretical Computer Science},
YEAR = 1975,
VOLUME = 1,
NUMBER = 2,
PAGES = {125--159}
}
@BOOK{Prawitz65,
AUTHOR = {D. Prawitz},
TITLE = {Natural deduction, a proof-theoretical study},
PUBLISHER = {Almquist and Wiksell},
YEAR = {1965}
}
@TECHREPORT{Saibi95,
AUTHOR = {A. Sa{\"\i}bi},
TITLE = {Une axiomatisation constructive
de la th\'eorie des cat\'egories},
INSTITUTION = {INRIA},
YEAR = 1995,
NOTE = {To appear as a research report}
}
@INPROCEEDINGS{Views,
AUTHOR = {Philip Wadler},
TITLE = {{Views: A way for pattern matching to cohabit with
data abstraction}},
BOOKTITLE = {14th ACM Symposium on Principles of
Programming Languages},
YEAR = 1987,
ADDRESS = {Munich},
MONTH = {January}
}
@PHDTHESIS{Werner94,
AUTHOR = {B. Werner},
TITLE = {Une {T}h\'eorie des {C}onstructions {I}nductives},
SCHOOL = {Universit\'e de Paris VII},
YEAR = 1994,
MONTH = {Mai},
TYPE = {Th\`ese de doctorat}
}
@MISC{ERA,
AUTHOR = {David Lester},
TITLE = {{Exact Arithmetic Implementations in Haskell and PVS proofs}},
NOTE = {\url{http://www.cs.man.ac.uk/arch/dlester/exact.html}}
}
@INPROCEEDINGS{Boehm86,
AUTHOR = {H. Boehm and R. Cartwright and M. J. O'Donnell and M. Riggle},
TITLE = {{Exact Real Arithmetic: A Case Study in Higher Order Programming}},
BOOKTITLE = {{Proceedings of the 1986 Lisp and Functional Programming Conference}},
PAGES = {162-173},
YEAR = 1986
}
@MISC{CRClass,
AUTHOR = {Hans Boehm},
TITLE = {{Exact Arithmetic Implementation in Java}},
NOTE = {\url{http://www.hpl.hp.com/personal/Hans_Boehm/crcalc/}}
}
This file has been generated by
bibtex2html 1.55