diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:48:32 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 14:27:21 +0100 |
commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /doc/faq | |
parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'doc/faq')
-rw-r--r-- | doc/faq/FAQ.tex | 16 | ||||
-rw-r--r-- | doc/faq/fk.bib | 126 |
2 files changed, 71 insertions, 71 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 647a151d7..5a6691072 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -14,7 +14,7 @@ %\usepackage{multicol} \usepackage{hevea} \usepackage{fullpage} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage[english]{babel} \ifpdf % si on est en pdflatex @@ -138,7 +138,7 @@ \large(\protect\ref{lastquestion} \ Hints) } -\author{Pierre Castéran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux} +\author{Pierre Castéran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux} \maketitle %%%%%%% @@ -254,7 +254,7 @@ notes~\cite{Types:Dowek}. \item[Inductive types] Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}. \item[Co-Inductive types] -Eduardo Giménez' thesis~\cite{EGThese}. +Eduardo Giménez' thesis~\cite{EGThese}. \item[Miscellaneous] A \ahref{http://coq.inria.fr/doc/biblio.html}{bibliography} about Coq \end{description} @@ -397,7 +397,7 @@ New versions of {\Coq} are announced on the coq-club mailing list. If you only w \Question{Is there any book about {\Coq}?} -The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004: +The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004: \begin{quote} ``This book provides a pragmatic introduction to the development of proofs and certified programs using \Coq. With its large collection of @@ -1124,7 +1124,7 @@ Qed. Just use the semi-decision tactic: \firstorder. \iffalse -todo: demander un exemple à Pierre +todo: demander un exemple à Pierre \fi \Question{My goal is solvable by a sequence of rewrites, how can I prove it?} @@ -1200,7 +1200,7 @@ Qed. \Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?} -You need the {\gb} tactic (see Loïc Pottier's homepage). +You need the {\gb} tactic (see Loïc Pottier's homepage). \subsection{Tactics usage} @@ -1265,7 +1265,7 @@ You can split your hint bases into smaller ones. \Question{What is the equivalent of {\tauto} for classical logic?} -Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation. +Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation. \Question{I want to replace some term with another in the goal, how can I do it?} @@ -1914,7 +1914,7 @@ Notation "x ^2" := (Rmult x x) (at level 20). \end{verbatim} Note that you can not use: \begin{tt} -Notation "x $^²$" := (Rmult x x) (at level 20). +Notation "x $^2$" := (Rmult x x) (at level 20). \end{tt} because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8. diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib index d41ab7f09..4d90efcdb 100644 --- a/doc/faq/fk.bib +++ b/doc/faq/fk.bib @@ -16,11 +16,11 @@ } @PHDTHESIS{EGThese, - author = {Eduardo Giménez}, + author = {Eduardo Giménez}, title = {Un Calcul de Constructions Infinies et son application -a la vérification de systèmes communicants}, - type = {thèse d'Université}, - school = {Ecole Normale Supérieure de Lyon}, +a la vérification de systèmes communicants}, + type = {thèse d'Université}, + school = {Ecole Normale Supérieure de Lyon}, month = {December}, year = {1996}, } @@ -29,7 +29,7 @@ a la vérification de systèmes communicants}, %%%%%%% Semantique %%%%%%% @misc{Sem:cours, - author = "François Pottier", + author = "François Pottier", title = "{Typage et Programmation}", year = "2002", howpublished = "Lecture notes", @@ -109,7 +109,7 @@ year = {1981} @book{Coq:coqart, title = "Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions", - author = "Yves Bertot and Pierre Castéran", + author = "Yves Bertot and Pierre Castéran", publisher = "Springer Verlag", series = "Texts in Theoretical Computer Science. An EATCS series", @@ -118,8 +118,8 @@ year = {1981} @phdthesis{Coq:Del01, AUTHOR = "David Delahaye", - TITLE = "Conception de langages pour décrire les preuves et les - automatisations dans les outils d'aide à la preuve", + TITLE = "Conception de langages pour décrire les preuves et les + automatisations dans les outils d'aide à la preuve", SCHOOL = {Universit\'e Paris~6}, YEAR = "2001", Type = {Th\`ese de Doctorat} @@ -133,7 +133,7 @@ year = {1981} url = "citeseer.nj.nec.com/gimenez98tutorial.html" } @phdthesis{Coq:Mun97, - AUTHOR = "César Mu{\~{n}}oz", + AUTHOR = "César Mu{\~{n}}oz", TITLE = "Un calcul de substitutions pour la repr\'esentation de preuves partielles en th\'eorie de types", SCHOOL = {Universit\'e Paris~7}, @@ -191,7 +191,7 @@ year = {1981} } @misc{PVS-Tactics:cours, - author = "César Muñoz", + author = "César Muñoz", title = "Strategies in {PVS}", howpublished = "Lecture notes", note = "National Institute of Aerospace", @@ -288,9 +288,9 @@ year = {1981} } @TECHREPORT{modelpa2000, - AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg + AUTHOR = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg and J.-F. Monin and C. Paulin and A. Petit and D. Rouillard}, - TITLE = {Automates temporisés CALIFE}, + TITLE = {Automates temporisés CALIFE}, INSTITUTION = {Calife}, YEAR = 2000, URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F1.1.ps.gz}, @@ -298,8 +298,8 @@ year = {1981} } @TECHREPORT{CaFrPaRo2000, - AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard}, - TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates}, + AUTHOR = {P. Castéran and E. Freund and C. Paulin and D. Rouillard}, + TITLE = {Bibliothèques Coq et Isabelle-HOL pour les systèmes de transitions et les p-automates}, INSTITUTION = {Calife}, YEAR = 2000, URL = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F5.4.ps.gz}, @@ -335,7 +335,7 @@ year = {1981} MONTH = JAN, SCHOOL = {{Paris 7}}, TITLE = {Extraction de programmes dans le {Calcul des Constructions}}, - TYPE = {Thèse d'université}, + TYPE = {Thèse d'université}, YEAR = {1989}, URL = {http://www.lri.fr/~paulin/these.ps.gz} } @@ -427,11 +427,11 @@ nd Applications}, @PHDTHESIS{Pau96b, AUTHOR = {Christine Paulin-Mohring}, - TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur}, - SCHOOL = {Université Claude Bernard Lyon I}, + TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur}, + SCHOOL = {Université Claude Bernard Lyon I}, YEAR = 1996, MONTH = DEC, - TYPE = {Habilitation à diriger les recherches}, + TYPE = {Habilitation à diriger les recherches}, URL = {http://www.lri.fr/~paulin/habilitation.ps.gz} } @@ -488,7 +488,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, } @TECHREPORT{kmu2002rr, - AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain}, + AUTHOR = {Keiichirou Kusakari and Claude Marché and Xavier Urbain}, TITLE = {Termination of Associative-Commutative Rewriting using Dependency Pairs Criteria}, INSTITUTION = {LRI}, YEAR = 2002, @@ -509,7 +509,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, } @INPROCEEDINGS{contejean03wst, - AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain}, + AUTHOR = {Evelyne Contejean and Claude Marché and Benjamin Monate and Xavier Urbain}, TITLE = {{Proving Termination of Rewriting with {\sc C\textit{i}ME}}}, CROSSREF = {wst03}, PAGES = {71--73}, @@ -661,7 +661,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, YEAR = {2003}, EDITOR = {Albert Rubio}, MONTH = JUN, - NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain} + NOTE = {Technical Report DSIC II/15/03, Universidad Politécnica de Valencia, Spain} } @INPROCEEDINGS{FilliatreLetouzey03, @@ -740,8 +740,8 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, @INPROCEEDINGS{Filliatre01a, AUTHOR = {J.-C. Filli\^atre}, - TITLE = {La supériorité de l'ordre supérieur}, - BOOKTITLE = {Journées Francophones des Langages Applicatifs}, + TITLE = {La supériorité de l'ordre supérieur}, + BOOKTITLE = {Journées Francophones des Langages Applicatifs}, PAGES = {15--26}, MONTH = {Janvier}, YEAR = 2002, @@ -749,18 +749,18 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, URL = {http://www.lri.fr/~filliatr/ftp/publis/sos.ps.gz}, CODE = {http://www.lri.fr/~filliatr/ftp/ocaml/misc/koda-ruskey.ps}, ABSTRACT = { - Nous présentons ici une écriture fonctionnelle de l'algorithme de + Nous présentons ici une écriture fonctionnelle de l'algorithme de Koda-Ruskey, un algorithme pour engendrer une large famille de codes de Gray. En s'inspirant de techniques de programmation par - continuation, nous aboutissons à un code de neuf lignes seulement, - bien plus élégant que les implantations purement impératives - proposées jusqu'ici, notamment par Knuth. Dans un second temps, - nous montrons comment notre code peut être légèrement modifié pour - aboutir à une version de complexité optimale. - Notre implantation en Objective Caml rivalise d'efficacité avec les - meilleurs codes C. Nous détaillons les calculs de complexité, - un exercice intéressant en présence d'ordre supérieur et d'effets de - bord combinés.} + continuation, nous aboutissons à un code de neuf lignes seulement, + bien plus élégant que les implantations purement impératives + proposées jusqu'ici, notamment par Knuth. Dans un second temps, + nous montrons comment notre code peut être légèrement modifié pour + aboutir à une version de complexité optimale. + Notre implantation en Objective Caml rivalise d'efficacité avec les + meilleurs codes C. Nous détaillons les calculs de complexité, + un exercice intéressant en présence d'ordre supérieur et d'effets de + bord combinés.} } @TECHREPORT{Filliatre00c, @@ -901,33 +901,33 @@ and Erik Poll and Nicole Rauch and Xavier Urbain}, YEAR = 1999, MONTH = {July}, URL = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}, - ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant - traits impératifs et fonctionnels dans le cadre de la théorie des + ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant + traits impératifs et fonctionnels dans le cadre de la théorie des types. - La théorie des types constitue un puissant langage de spécification, - naturellement adapté à la preuve de programmes purement - fonctionnels. Pour y certifier également des programmes impératifs, - nous commençons par exprimer leur sémantique de manière purement + La théorie des types constitue un puissant langage de spécification, + naturellement adapté à la preuve de programmes purement + fonctionnels. Pour y certifier également des programmes impératifs, + nous commençons par exprimer leur sémantique de manière purement fonctionnelle. Cette traduction repose sur une analyse statique des effets de bord des programmes, et sur l'utilisation de la notion de - monade, notion que nous raffinons en l'associant à la notion d'effet - de manière générale. Nous montrons que cette traduction est - sémantiquement correcte. - - Puis, à partir d'un programme annoté, nous construisons une preuve - de sa spécification, traduite de manière fonctionnelle. Cette preuve - est bâtie sur la traduction fonctionnelle précédemment - introduite. Elle est presque toujours incomplète, les parties - manquantes étant autant d'obligations de preuve qui seront laissées - à la charge de l'utilisateur. Nous montrons que la validité de ces - obligations entraîne la correction totale du programme. - - Nous avons implanté notre travail dans l'assistant de preuve - Coq, avec lequel il est dès à présent distribué. Cette - implantation se présente sous la forme d'une tactique prenant en - argument un programme annoté et engendrant les obligations de - preuve. Plusieurs algorithmes non triviaux ont été certifiés à + monade, notion que nous raffinons en l'associant à la notion d'effet + de manière générale. Nous montrons que cette traduction est + sémantiquement correcte. + + Puis, à partir d'un programme annoté, nous construisons une preuve + de sa spécification, traduite de manière fonctionnelle. Cette preuve + est bâtie sur la traduction fonctionnelle précédemment + introduite. Elle est presque toujours incomplète, les parties + manquantes étant autant d'obligations de preuve qui seront laissées + à la charge de l'utilisateur. Nous montrons que la validité de ces + obligations entraîne la correction totale du programme. + + Nous avons implanté notre travail dans l'assistant de preuve + Coq, avec lequel il est dès à présent distribué. Cette + implantation se présente sous la forme d'une tactique prenant en + argument un programme annoté et engendrant les obligations de + preuve. Plusieurs algorithmes non triviaux ont été certifiés à l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de Knuth-Morris-Pratt).} } @@ -1081,7 +1081,7 @@ tique}, } @InCollection{cc, - author = {Thierry Coquand and Gérard Huet}, + author = {Thierry Coquand and Gérard Huet}, title = {The Calculus of Constructions}, booktitle = {Information and Computation}, year = {1988}, @@ -1095,7 +1095,7 @@ tique}, title = {Inductively defined types}, booktitle = {Proceedings of Colog'88}, year = {1990}, - editor = {P. Martin-Löf and G. Mints}, + editor = {P. Martin-Löf and G. Mints}, volume = {417}, series = {LNCS}, publisher = {Springer-Verlag} @@ -1318,7 +1318,7 @@ s}, } @INPROCEEDINGS{CoHu85a, - AUTHOR = {Thierry Coquand and Gérard Huet}, + AUTHOR = {Thierry Coquand and Gérard Huet}, ADDRESS = {Linz}, BOOKTITLE = {EUROCAL'85}, PUBLISHER = SV, @@ -1329,7 +1329,7 @@ s}, } @INPROCEEDINGS{CoHu85b, - AUTHOR = {Thierry Coquand and Gérard Huet}, + AUTHOR = {Thierry Coquand and Gérard Huet}, BOOKTITLE = {Logic Colloquium'85}, EDITOR = {The Paris Logic Group}, PUBLISHER = {North-Holland}, @@ -1338,7 +1338,7 @@ s}, } @ARTICLE{CoHu86, - AUTHOR = {Thierry Coquand and Gérard Huet}, + AUTHOR = {Thierry Coquand and Gérard Huet}, JOURNAL = {Information and Computation}, NUMBER = {2/3}, TITLE = {The {Calculus of Constructions}}, @@ -2092,7 +2092,7 @@ the Calculus of Inductive Constructions}}, @PHDTHESIS{Bar99, AUTHOR = {B. Barras}, SCHOOL = {Universit\'e Paris 7}, - TITLE = {Auto-validation d'un système de preuves avec familles inductives}, + TITLE = {Auto-validation d'un système de preuves avec familles inductives}, TYPE = {Th\`ese de Doctorat}, YEAR = {1999} } @@ -2177,7 +2177,7 @@ Decomposition}}, @Book{CoqArt, - author = {Yves bertot and Pierre Castéran}, + author = {Yves bertot and Pierre Castéran}, title = {Coq'Art}, publisher = {Springer-Verlag}, year = 2004, |