%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Matthieu Sozeau at 2008-12-14 16:11:16 +0100 


%% Saved with string encoding Unicode (UTF-8) 


@string{aaecc = {Applicable Algebra in Engineering Communication and    Computing}}

@string{acm = {ACM Press}}

@string{acmpress = {ACM Press}}

@string{addresslri = {Univ. Paris-Sud, France}}

@string{ai = {Artificial Intelligence}}

@string{alp90 = {Proc. 2nd Int. Conf. on Algebraic and Logic    Programming, LNCS 463}}

@string{alp92 = {Proc. 3rd Int. Conf. on Algebraic and Logic    Programming, LNCS 632}}

@string{alp94 = {Proc. 4th Int. Conf. on Algebraic and Logic                  Programming, LNCS 850}}

@string{alp96 = {Proc. 5th Int. Conf. on Algebraic and Logic                  Programming, LNCS 1139}}

@string{alpplilp98 = {Proc. Joint Int. Symp. on Programming         Languages,Implementations, Logics and Programs (PLILP) and         Algebraic and Logic Programming (ALP) conferences}}

@string{amm = {American Mathematical Monthly}}

@string{ap = {Academic Press}}

@string{aplas = {Asian Symposium on Programming Languages and Systems (APLAS)}}

@string{aplas03 = aplas # {, Beijing, China}}

@string{atopls = {ACM Transactions on Programming Languages and Systems}}

@string{aw = {Addison-Wesley}}

@string{beatcs = {EATCS Bulletin}}

@string{birk = {Birkh{\"a}user}}

@string{cacm = {Communications of the {ACM}}}

@string{cade80 = {Proc. 5th Conf. on Automated Deduction, Les Arcs,    France, LNCS 87}}

@string{cade84 = {Proc. 7th Int. Conf. on Automated Deduction, Napa,    LNCS 170}}

@string{cade86 = {Proc. 8th Int. Conf. on Automated Deduction, Oxford,    England, LNCS 230}}

@string{cade90 = {Proc. 10th Int. Conf. on Automated Deduction,    Kaiserslautern, LNCS 449}}

@string{cade92 = {Proc. 11th Int. Conf. on Automated Deduction,    Saratoga Springs, NY, LNAI 607}}

@string{cav = {International Conference on Computer Aided Verification (CAV)}}

@string{cav02 = cav # {, Copenhagen, Denmark}}

@string{cav96 = cav # {, New Brunswick, New Jersey}}

@string{ccl = {Constraints in Computational Logics}}

@string{ccl94 = {Proc. 1st Int. Conf. on Constraint in Computational     Logics, LNCS 845}}

@string{cecsl = {Conference of the European Association for Computer Science Logic}}

@string{crin = {Centre de Recherche en Informatique de Nancy}}

@string{csfw = {IEE Computer Security Foundations Workshop (CSFW) }}

@string{csfw02 = csfw # {, Cape Breton, Nova Scotia}}

@string{csl = {International Workshop on Computer Science Logic (CSL)}}

@string{csl93 = {Proc. Conf. Computer Science Logic}}

@string{csl94 = csl # {, Kazimierz, Poland}}

@string{csl95 = {Proc. Conf. Computer Science Logic}}

@string{csl97 = csl # {, Aarhus, Denmark}}

@string{ctrs90 = {Proc. 2nd Int. Workshop on Conditional and Typed    Rewriting Systems, Montreal, LNCS 516}}

@string{ctrs91 = {Proc. Conditional and Typed Rewriting Systems, LNCS 516}}

@string{ctrs92 = {Proc. 3rd Int. Workshop on Conditional Term    Rewriting Systems, Pont-{\`a}-Mousson, LNCS 656}}

@string{ctrs93 = {Proc. Conditional Term Rewriting Systems, LNCS 656}}

@string{cup = {Cambridge University Press}}

@string{cwi = {Centrum voor Wiskunde en Informatica}}

@string{dbpl = {Database Programming Languages (DBPL)}}

@string{dbpl05 = dbpl}

@string{diku = {University of Copenhagen, Department of Computer Science}}

@string{disc = {International Symposium on Distributed Computing (DISC)}}

@string{disc06 = disc}

@string{disco90 = {Proc. Int. Symposium on Design and Implementation    of Symbolic Computation Systems, LNCS 429}}

@string{dmtcs = {Discrete Mathematics and Theoretical Computer Science}}

@string{ecoop = {European Conference on Object-Oriented Programming (ECOOP)}}

@string{ecoop00 = ecoop # {, Sophia Antipolis and Cannes, France}}

@string{ecoop02 = ecoop # {, Malaga, Spain}}

@string{ecoop03 = ecoop # {, Darmstadt, Germany}}

@string{ecoop04 = ecoop # {, Oslo, Norway}}

@string{ecoop06 = ecoop # {, Nantes, France}}

@string{oopsla = {{ACM} {SIGPLAN} {C}onference on {O}bject {O}riented {P}rogramming:                     {S}ystems, {L}anguages, and {A}pplications ({OOPSLA})}}

@string{ecoop90 = oopsla # {/} # ecoop # {, Ottawa, Ontario}}

@string{ecoop92 = ecoop}

@string{ecoop95 = ecoop}

@string{ecoop98 = ecoop}

@string{ecoop99 = ecoop # {, Lisbon, Portugal}}

@string{elsevier = {Elsevier}}

@string{enslyon = {Ecole Normale Sup{\'e}rieure de Lyon}}

@string{ensparis = {Ecole Normale Sup{\'e}rieure de Paris}}

@string{entcs = {Electronic Notes in Theoretical Computer Science}}

@string{es = {Elsevier Science Publishers}}

@string{esop = {European Symposium on Programming (ESOP)}}

@string{esop00 = esop # {, Berlin, Germany}}

@string{esop01 = esop # {, Genova, Italy}}

@string{esop02 = esop # {, Grenoble, France}}

@string{esop88 = esop # {, Nancy, France}}

@string{esop92 = esop # {, Rennes, France}}

@string{esop94 = esop # {, Edinburgh, Scotland}}

@string{eup = {Edinburgh Univ. Press}}

@string{fac = {Formal Aspect of Computing}}

@string{flops = {International Symposium on Functional and Logic Programming (FLOPS)}}

@string{flops04 = flops # {, Nara, Japan}}

@string{informal = {{\rm, informal proceedings}}}

@string{fool = {International Workshop on Foundations of Object-Oriented Languages (FOOL)} # informal}

@string{fpca = {ACM Symposium on Functional Programming Languages and                     Computer Architecture (FPCA)}}

@string{fpca87 = fpca # {, Portland, Oregon}}

@string{fpca89 = fpca # {, London, England}}

@string{fpca93 = fpca # {, Copenhagen, Denmark}}

@string{fpca95 = fpca # {San Diego, California}}

@string{frr = {Rapport de Recherche}}

@string{fsttcs = {Foundations of Software Technology and Theoretical Computer Science (FSTTCS)}}

@string{fsttcs93 = fsttcs # {, Bombay, India}}

@string{greco = {Greco de Programmation}}

@string{gtm = {Graduate Texts in Mathematics}}

@string{haskellw = {ACM Haskell Workshop} # informal}

@string{hoots = {Workshop on Higher Order Operational Techniques in Semantics (HOOTS)}}

@string{iandcomp = {Information and Computation}}

@string{ic = {Information and Computation}}

@string{icalp = {International Colloquium on Automata, Languages and Programming (ICALP)}}

@string{icalp77 = {Proc. 4th Int. Coll. on Automata, Languages and    Programming, Turku, Finland}}

@string{icalp78 = {Proc. 5th Int. Coll. on Automata, Languages and    Programming, LNCS 62}}

@string{icalp82 = {Proc. 9th Int. Coll. on Automata, Languages and    Programming, LNCS 140}}

@string{icalp83 = {Proc. 10th Int. Coll. on Automata, Languages and    Programming, LNCS 154}}

@string{icalp85 = {Proc. 12th Int. Coll. on Automata, Languages and    Programming, Nafplion, LNCS 194}}

@string{icalp87 = {Proc. 14th Int. Coll. on Automata, Languages and    Programming, LNCS 372}}

@string{icalp88 = {Proc. 15th Int. Coll. on Automata, Languages and    Programming, LNCS 317}}

@string{icalp89 = {Proc. 16th Int. Coll. on Automata, Languages and    Programming, LNCS 372}}

@string{icalp90 = {Proc. 17th Int. Coll. on Automata, Languages and    Programming, Warwick, LNCS 443}}

@string{icalp91 = {Proc. 18th Int. Coll. on Automata, Languages and    Programming, Madrid, LNCS 510}}

@string{icalp92 = {Proc. 19th Int. Coll. on Automata, Languages and    Programming, LNCS 623}}

@string{icalp93 = {Proc. 20th Int. Coll. on Automata, Languages and    Programming, LNCS 700}}

@string{icalp94 = {Proc. 21th Int. Coll. on Automata, Languages and                  Programming, LNCS 820}}

@string{icalp98 = icalp # {, Aalborg, Denmark}}

@string{icalp99 = {Proc. 25th Int. Coll. on Automata, Languages and                  Programming, To appear}}

@string{icfp = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming                     ({ICFP})}}

@string{icfp00 = icfp # {, Montreal, Canada}}

@string{icfp01 = icfp # {, Firenze, Italy}}

@string{icfp02 = icfp # {, Pittsburgh, Pennsylvania}}

@string{icfp03 = icfp # {, Uppsala, Sweden}}

@string{icfp04 = icfp # {, Snowbird, Utah}}

@string{icfp96 = icfp # {, Philadelphia, Pennsylvania}}

@string{icfp97 = icfp # {, Amsterdam, The Netherlands}}

@string{icfp98 = icfp # {, Baltimore, Maryland}}

@string{icfp99 = icfp # {, Paris, France}}

@string{icomp = {Information and Computation}}

@string{icont = {Information and Control}}

@string{ieeecsp = {{IEEE} Comp. Soc. Press}}

@string{ieeetcom = {IEEE Trans. Communications}}

@string{ieice = {IEICE}}

@string{ijait = {International Journal on Artificial Intelligence Tools}}

@string{ijcis = {International Journal of Computer and Information    Sciences}}

@string{ijfcs = {International Journal of Foundations of Computer    Science}}

@string{ijpp = {International Journal on Parallel Programming}}

@string{inpg = {Institut National Polytechnique de Grenoble}}

@string{inria = {Institut National de Recherche en Informatique et en     Automatique, Unit{\'e} Rocquencourt}}

@string{ipl = {Information Processing Letters}}

@string{issac88 = {Proc. of the 19th Int. Symp. on Symbolic and    Algebraic Computation}}

@string{issac89 = {Proc. of the 20th Int. Symp. on Symbolic and    Algebraic Computation, Portland, Oregon}}

@string{ja = {Journal of Algebra}}

@string{jacm = {Journal of the {ACM}}}

@string{jar = {Journal of Automated Reasoning}}

@string{jcss = {Journal of Computer and System Sciences}}

@string{jfla = {Journ{\'e}es Francophones des Langages Applicatifs}}

@string{jflp = {Journal of Functional and Logic Programming}}

@string{jfp = {Journal of Functional Programming}}

@string{jlap = {Journal of Logic and Algebraic Programming}}

@string{jlc = {Journal of Logic and Computation}}

@string{jlp = {Journal of Logic Programming}}

@string{jmcm = {Journal of {M}athematical and Computer Modelling}}

@string{jpaa = {Journal of Pure and Applied Algebra}}

@string{jsc = {Journal of Symbolic Computation}}

@string{jsl = {Journal of Symbolic Logic}}

@string{labri = {LAboratoire Bordelais de Recherche en Informatique}}

@string{lfcompsci = {International Symposium on Logical Foundations of Computer Science (LFCS)}}

@string{lfcompsci94 = lfcompsci # {, St. Petersburg, Russia}}

@string{lfcs = {Laboratory for Foundations of Computer Science,                     University of Edinburgh}}

@string{lfp = {ACM Symposium on Lisp and Functional Programming (LFP)}}

@string{lfp80 = lfp # {, Stanford, California}}

@string{lfp84 = lfp # {, Austin, Texas}}

@string{lfp86 = lfp # {, Cambridge, Massachusetts}}

@string{lfp88 = lfp # {, Snowbird, Utah}}

@string{lfp90 = lfp}

@string{lfp92 = lfp # {, San Francisco, California}}

@string{lfp94 = lfp # {, Orlando, Florida}}

@string{lics = {IEEE Symposium on Logic in Computer Science (LICS)}}

@string{lics00 = lics}

@string{lics01 = lics # {, Boston, Massachusetts}}

@string{lics02 = lics}

@string{lics03 = lics # {, Ottawa, Canada}}

@string{lics1 = {Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge,    Mass.}}

@string{lics2 = {Proc. 2nd IEEE Symp. Logic in Computer Science, Ithaca, NY}}

@string{lics3 = {Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh}}

@string{lics4 = {Proc. 4th IEEE Symp. Logic in Computer Science}}

@string{lics5 = {Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia}}

@string{lics6 = {Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam}}

@string{lics7 = {Proc. 7th IEEE Symp. Logic in Computer Science, Santa Cruz}}

@string{lics86 = lics # {, Cambridge, Massachusetts}}

@string{lics87 = lics # {, Ithaca, New York}}

@string{lics88 = lics # {, Edinburgh, Scotland}}

@string{lics89 = lics # {, Asilomar, California}}

@string{lics90 = lics # {, Philadelphia, Pennsylvania}}

@string{lics91 = lics}

@string{lics92 = lics # {, Santa Cruz, California}}

@string{lics93 = lics}

@string{lics94 = lics}

@string{lics95 = lics}

@string{lics96 = lics # {, New Brunswick, New Jersey}}

@string{lics97 = lics}

@string{lics98 = lics # {, Indianapolis, Indiana}}

@string{lics99 = lics # {, Trento, Italy}}

@string{liens = {Laboratoire d'Informatique de l'{\'E}cole Normale Sup{\'e}rieure}}

@string{lifo = {Laboratoire d'Informatique Fondamentale d'Orl{\'e}ans}}

@string{lip = {Laboratoire de l'Informatique du Parallelisme}}

@string{lnai = {Lecture Notes in Artificial Intelligence}}

@string{lncs = {Lecture Notes in Computer Science}}

@string{lncs104 = {Proc. 5th GI Conf., LNCS 104}}

@string{lncs107 = {Int. Coll. Formalization of Programming Concepts,    LNCS 107}}

@string{lncs131 = {Proc. IBM Workshop on Logics of Programs, LNCS    131}}

@string{lncs137 = {Proc. 5th Int. Symp. on Programming, Turin, LNCS    137}}

@string{lncs144 = {Proc. EUROCAM 82, Marseille, LNCS 144}}

@string{lncs145 = {Proc. 6th GI Conf.}}

@string{lncs159 = {Proc. 8th. Coll. on Trees and Algebra in    Programming, LNCS 159}}

@string{lncs164 = {Proc. Logics of Programming Workshop}}

@string{lncs173 = {Semantics of Data Types, Sophia-Antipolis, LNCS    173}}

@string{lncs174 = {Proc. EUROSAM 84, Cambridge, LNCS 174}}

@string{lncs185 = {Proc. CAAP 85, LNCS 185}}

@string{lncs197 = {Seminar on Concurrency, CMU-Pittsburgh, LNCS 197}}

@string{lncs201 = {Functional Programming Languages and Computer    Architecture, Nancy, LNCS 201}}

@string{lncs202 = {Proc. Rewriting Techniques and Applications 85, Dijon, LNCS 202}}

@string{lncs203 = {Proc. EUROCAL 85, Linz, LNCS 203}}

@string{lncs204 = {Proc. EUROCAL 85, Linz, LNCS 204}}

@string{lncs210 = {Proc. STACS 86, Orsay, LNCS 210}}

@string{lncs213 = {Proc. ESOP 86, Saarbr{\"u}cken, LNCS 213}}

@string{lncs214 = {Proc. CAAP 86, Nice, LNCS 214}}

@string{lncs217 = {Programs as Data Objects, Copenhagen, LNCS 217}}

@string{lncs226 = {Proc. 13th ICALP, Rennes, LNCS 226}}

@string{lncs230 = {Proc. 8th Conf. on Automated Deduction, Oxford, LNCS 230}}

@string{lncs232 = {Fundamentals of Artificial Intelligence, LNCS 232}}

@string{lncs233 = {Proc. Math. Found. Computer Science, Bratislava, LNCS 233}}

@string{lncs241 = {Proc. 6th Conf. on Foundations of Software    Technology and Theoretical Computer Science, New    Delhi, LNCS 241}}

@string{lncs249 = {Proc. CAAP 87, Pisa, LNCS 249}}

@string{lncs250 = {Proc. CFLP, Pisa, LNCS 250}}

@string{lncs255 = {Petri Nets: Applications and Relationships to Other    Models of Concurrency, Bad Honnef, LNCS 255}}

@string{lncs258 = {Proc. PARLE 87, vol. I: Parallel Architectures,    Eindhoven, LNCS 258}}

@string{lncs259 = {Proc. PARLE 87, vol. II: Parallel Languages,    Eindhoven, LNCS 259}}

@string{lncs272 = {Future Parallel Computers, an advanced course,    Pisa, LNCS 272}}

@string{lncs283 = {Proc. Category Theory and Computer Science, LNCS    283}}

@string{lncs287 = {Proc. 7th Conf. Found. of Software Technology and    Theoretical Computer Science, Pune, INDIA, LNCS 287}}

@string{lncs294 = {Proc. STACS 88, Bordeaux, LNCS 294}}

@string{lncs298 = {Proc. 3rd Workshop on Mathematical Foundations of    Programming Language Semantics, LNCS 298}}

@string{lncs299 = {Proc. CAAP 88, Nancy, LNCS 299}}

@string{lncs300 = {Proc. ESOP 88, Nancy, LNCS 300}}

@string{lncs306 = {Proc. Workshop on Found. of Logic and Functional    Programming, Trento, LNCS 306}}

@string{lncs308 = {Proc. 1st Int. Workshop on Conditional Term    Rewriting Systems, Orsay, LNCS 308}}

@string{lncs332 = {Recent Trends in Data Type Specifications, S.    Sanella and A. Tarleki eds., LNCS 332}}

@string{lncs343 = {Proc. 1st Workshop on Algebraic and Logic    Programming, Gaussig, LNCS 343}}

@string{lncs349 = {Proc. STACS 89, Paderborn, LNCS 349}}

@string{lncs351 = {Proc. TAPSOFT 89 (Vol. 1), Barcelona, LNCS 351}}

@string{lncs352 = {Proc. TAPSOFT 89 (Vol. 2), Barcelona, LNCS 352}}

@string{lncs354 = {Linear Time, Branching Time and Partial Order in    Logics and Models for Concurrency, Noordwijkerhout,    LNCS 354}}

@string{lncs380 = {Proc. FCT'89, LNCS 380}}

@string{lncs415 = {Proc. STACS 90, Rouen, LNCS 415}}

@string{lncs431 = {Proc. CAAP 90, Copenhague, LNCS 431}}

@string{lncs432 = {Proc. ESOP 90, Copenhague, LNCS 432}}

@string{lncs452 = {Proc. MFCS 90, Bansk{\`{a}} Bystrica, LNCS 452}}

@string{lncs456 = {Proc. PLILP'90, LNCS 456}}

@string{lncs463 = {Proc. Conf. on Algebraic and Logic Programming,    Nancy, LNCS 463}}

@string{lncs480 = {Proc. 8th Symp. on Theoretical Aspects of Computer    Science, Hamburg, LNCS 480}}

@string{lncs493 = {Proc. TAPSOFT'91---CAAP, LNCS 493}}

@string{lncs535 = {Fundamentals of Artificial Intelligence, P. Jorrand    Editor, LNCS 535}}

@string{lncs582 = {Proc. European Symp. on Programming, LNCS 582}}

@string{lncs59 = {Proc. Proc. Eight Colloquium on Trees in Algebra and    Programming, LNCS 59}}

@string{lncs78 = {Edinburgh LCF, LNCS 78}}

@string{lncs86 = {Proc. Winter School on Abstract Software    Specifications, Copenhagen, LNCS 86}}

@string{lncs99 = {Algebraic Semantics, LNCS 99}}

@string{lncs996 = {Proc. of the 1994 Workshop on Types for Proofs and                     Programs, LNCS 996}}

@string{lnm = {Lecture Notes in Mathematics}}

@string{lp = {Lisp Pointers}}

@string{lri = {Laboratoire de Recherche en Informatique}}

@string{mcgh = {McGraw-Hill}}

@string{me = {Matthieu Sozeau}}

@string{mfcs15 = {Proc. 15th Mathematical Foundations of Computer    Science, Bansk{\`a} Bystrica}}

@string{mfcs16 = {Proc. 16th Mathematical Foundations of Computer    Science, Warsaw, LNCS 520}}

@string{mfcs92 = {Proc. 17th Mathematical Foundations of Computer    Science, Praha, LNCS}}

@string{mfcs93 = {Proc. 18th Mathematical Foundations of Computer                  Science}}

@string{mfcs98 = {Proc. 23rd Mathematical Foundations of Computer Science}}

@string{mfps = {Workshop on the Mathematical Foundations of Programming Semantics (MFPS)}}

@string{mfps01 = mfps # {, Aarhus, Denmark}}

@string{mfps89 = mfps # {, New Orleans, Louisiana}}

@string{mfps95 = mfps # {, New Orleans, Louisiana}}

@string{mgh = {McGraw-Hill}}

@string{mit = {MIT Press}}

@string{mp = {MIT Press}}

@string{mitpress = mp}

@string{mlw = {ACM SIGPLAN Workshop on ML} # informal}

@string{mpi = {Max-Planck-Institut f{\"u}r Informatik}}

@string{mpri = {Master Parisien de Recherche en Informatique}}

@string{mscs = {Mathematical Structures in Computer Science}}

@string{mst = {Math. Systems Theory}}

@string{nh = {North Holland}}

@string{no = {No}}

@string{oopsla03 = oopsla # {, Anaheim, California}}

@string{oopslapre96 = {{C}onference on {O}bject {O}riented {P}rogramming:                     {S}ystems, {L}anguages, and {A}pplications ({OOPSLA})}}

@string{oopsla86 = oopslapre96 # {, Portland, Oregon}}

@string{oopsla89 = oopslapre96 # {, New Orleans, Louisiana}}

@string{oopsla90 = oopslapre96 # {/} # ecoop # {, Ottawa, Ontario}}

@string{oopsla98 = oopsla # {, Vancouver, British Columbia}}

@string{orsay = {Orsay, France}}

@string{osdi = {USENIX Symposium on Operating Systems Design and Implementation (OSDI)}}

@string{osdi00 = osdi # {, San Diego, California}}

@string{osdi96 = osdi # {, Seattle, Washington}}

@string{paste = {ACM SIGPLAN--SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE)}}

@string{paste01 = paste # {, Snowbird, Utah}}

@string{ph = {Prentice Hall}}

@string{phd = {phd thesis}}

@string{pldi = {{ACM SIGPLAN Conference on Programming Language Design                     and Implementation (PLDI)}}}

@string{pldi00 = pldi # {, Vancouver, British Columbia, Canada}}

@string{pldi01 = pldi # {, Snowbird, Utah}}

@string{pldi02 = pldi # {, Berlin, Germany}}

@string{pldi03 = pldi # {, San Diego, California}}

@string{pldi88 = pldi # {, {A}tlanta, {G}eorgia}}

@string{pldi89 = pldi # {, Portland, Oregon}}

@string{pldi90 = pldi # {, White Plains, New York}}

@string{pldi91 = pldi # {, Toronto, Ontario}}

@string{pldi92 = pldi # {, San Francisco, California}}

@string{pldi93 = pldi # {, Albuquerque, New Mexico}}

@string{pldi94 = pldi # {, Orlando, Florida}}

@string{pldi95 = pldi # {, La Jolla, California}}

@string{pldi96 = pldi # {, Philadephia, Pennsylvania}}

@string{pldi97 = pldi # {, Las Vegas, Nevada}}

@string{pldi99 = pldi # {, {A}tlanta, {G}eorgia}}

@string{pods = {Principles of Database Systems (PODS)}}

@string{pods06 = pods}

@string{popl = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming                      {L}anguages ({POPL})}}

@string{popl00 = popl # {, Boston, Massachusetts}}

@string{popl01 = popl # {, London, England}}

@string{popl02 = popl # {, Portland, Oregon}}

@string{popl03 = popl # {, New Orleans, Louisiana}}

@string{popl04 = popl # {, Venice, Italy}}

@string{popl05 = popl # {, Long Beach, California}}

@string{popl08 = popl # {, San Francisco, California}}

@string{popl10 = {Proc. 10th ACM Symp. on Principles of Programming    Languages, Austin, Texas}}

@string{popl11 = {Proc. 11th ACM Symp. on Principles of Programming    Languages, Salt Lake City}}

@string{popl12 = {Proc. 12th ACM Symp. on Principles of Programming    Languages, New Orleans}}

@string{popl13 = {Proc. 13th ACM Symp. on Principles of Programming    Languages, St. Petersburg Beach, Florida}}

@string{popl14 = {Proc. 14th ACM Symp. on Principles of Programming    Languages, Munich}}

@string{popl15 = {Proc. 15th ACM Symp. on Principles of Programming    Languages, San Diego, California}}

@string{popl3 = {Proc. 3rd ACM Symp. on Principles of Programming    Languages, Atlanta}}

@string{popl5 = {Proc. 5th ACM Symp. on Principles of Programming    Languages, Tucson, Arizona}}

@string{popl6 = {Proc. 6th ACM Symp. on Principles of Programming    Languages, San Antonio, Texas}}

@string{popl7 = {Proc. 7th ACM Symp. on Principles of Programming    Languages, Las Vegas}}

@string{poplpre92 = {{ACM} {S}ymposium on {P}rinciples of {P}rogramming                      {L}anguages ({POPL})}}

@string{popl73 = poplpre92 # {, Boston, Massachusetts}}

@string{popl75 = poplpre92 # {, Palo Alto, California}}

@string{popl76 = poplpre92 # {, {A}tlanta, {G}eorgia}}

@string{popl77 = poplpre92 # {, Los Angeles, California}}

@string{popl78 = poplpre92 # {, Tucson, Arizona}}

@string{popl79 = poplpre92 # {, San Antonio, Texas}}

@string{popl80 = poplpre92 # {, Las Vegas, Nevada}}

@string{popl81 = poplpre92 # {, Williamsburg, Virginia}}

@string{popl82 = poplpre92 # {, Albuquerque, New Mexico}}

@string{popl83 = poplpre92 # {, Austin, Texas}}

@string{popl84 = poplpre92 # {, Salt Lake City, Utah}}

@string{popl85 = poplpre92 # {, New Orleans, Louisiana}}

@string{popl86 = poplpre92 # {, St.\ Petersburg Beach, Florida}}

@string{popl87 = poplpre92 # {, Munich, Germany}}

@string{popl88 = poplpre92 # {, San Diego, California}}

@string{popl89 = poplpre92 # {, Austin, Texas}}

@string{popl9 = {Proc. 9th ACM Symp. on Principles of Programming    Languages, Albuquerque, New Mexico}}

@string{popl90 = poplpre92 # {, {S}an {F}rancisco, {C}alifornia}}

@string{popl91 = poplpre92 # {, Orlando, Florida}}

@string{popl92 = popl # {, Albuquerque, New Mexico}}

@string{popl93 = popl # {, Charleston, South Carolina}}

@string{popl94 = popl # {, {P}ortland, {O}regon}}

@string{popl95 = popl # {, San Francisco, California}}

@string{popl96 = popl # {, St.~Petersburg Beach, Florida}}

@string{popl97 = popl # {, Paris, France}}

@string{popl98 = popl # {, San Diego, California}}

@string{popl99 = popl # {, San Antonio, Texas}}

@string{pp = {Pergamon Press}}

@string{ppdp = {ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP)}}

@string{ppdp01 = ppdp # {, Firenze, Italy}}

@string{ppdp99 = ppdp # {, Paris France}}

@string{proc = {Proceedings of the}}

@string{r = {Reidel}}

@string{rairo = {R.A.I.R.O.}}

@string{ria = {Revue Fran{\c{c}}aise d'Intelligence Artificielle}}

@string{rr = {Research Report}}

@string{rta = {International Conference on Rewriting Techniques and Applications (RTA)}}

@string{rta03 = rta # {, Valencia, Spain}}

@string{rta85 = {Proc. 1st Rewriting Techniques and Applications,    Dijon, LNCS 202}}

@string{rta87 = {Proc. 2nd Rewriting Techniques and Applications,    Bordeaux, LNCS 256}}

@string{rta89 = {Proc. 3rd Rewriting Techniques and Applications,    Chapel Hill, LNCS 355}}

@string{rta91 = {Proc. 4th Rewriting Techniques and Applications,    LNCS 488}}

@string{rta93 = {Proc. 5th Rewriting Techniques and Applications,    Montr{\'e}al, LNCS 690}}

@string{rta95 = {Proc. 6th Rewriting Techniques and Applications,    Kaiserslautern, LNCS 914}}

@string{rta96 = {Proc. 7th Rewriting Techniques and Applications,                  New Jersey}}

@string{sa = {Scientific American}}

@string{sas = {International Symposium on Static Analysis (SAS) }}

@string{sas01 = sas # {, Paris, France}}

@string{sas95 = sas # {, Glasgow, Scotland}}

@string{sas96 = sas # {, Aachen, Germany}}

@string{sas97 = sas # {, Paris, France}}

@string{scp = {Science of Computer Programming}}

@string{siamjc = {SIAM Journal on Computing}}

@string{sicomp = {SIAM Journal on Computing}}

@string{signot = {SIGPLAN Notices}}

@string{sosp = {ACM Symposium on Operating Systems Principles (SOSP)}}

@string{sosp93 = sosp # {, Asheville, North Carolina}}

@string{space = {Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE)} # informal}

@string{spe = {Software - Practice and Experience}}

@string{springer = {Springer-Verlag}}

@string{ssl93 = {Proc. Int. Workshop on Semantics of Specification Languages, Utrecht, October 1993}}

@string{stacs93 = {Proc. 10th Symposium on Theoretical Aspects of    Computer Science, W{\"u}rzburg, LNCS}}

@string{sv = {Springer-Verlag}}

@string{symsac = {Proc. ACM Symp. Symbolic and Algebraic Computation}}

@string{symsac71 = {Proc. of the 2nd Symp. on Symbolic and Algebraic    Computation}}

@string{symsac86 = {Proc. of the 17th Symp. on Symbolic and Algebraic    Computation}}

@string{tacs = {International Symposium on Theoretical Aspects of Computer Software (TACS)}}

@string{tacs01 = tacs # {, Sendai, Japan}}

@string{tacs94 = tacs # {, Sendai, Japan}}

@string{taoop = {C. A. Gunter and J. C. Mitchell, editors, {\em                     Theoretical Aspects of Object-Oriented Programming:                     Types, Semantics, and Language Design}, MIT Press, 1994}}

@string{tapsoft = {Theory and Practice of Software Development (TAPSOFT)}}

@string{tapsoft93 = tapsoft # {, Orsay, France}}

@string{tapsoft97 = tapsoft # {, Lille, France}}

@string{tcs = {Theoretical Computer Science}}

@string{these = {Th{\`e}se de Doctorat}}

@string{thesedoctorat = {Th{\`e}se de Doctorat}}

@string{theseh = {Th{\`e}se d'habilitation}}

@string{theseinpg = {Th{\`e}se de Doctorat, Institut National    Polytechnique de Grenoble, France}}

@string{theselri = {Th{\`e}se de Doctorat, Universit{\'e} de    Paris-Sud, France}}

@string{thesenancy = {Th{\`e}se de Doctorat, Universit{\'e} de Nancy    I, France}}

@string{tic = {ACM SIGPLAN Workshop on Types in Compilation ({TIC})}}

@string{tic97 = tic # {, Amsterdam, The Netherlands}}

@string{tic98 = tic # {, Kyoto, Japan}}

@string{tlca = {International Conference on Typed Lambda Calculi and Applications (TLCA)}}

@string{tlca01 = tlca # {, Krak{\'{o}}ow, Poland}}

@string{tlca03 = tlca # {, Valencia, Spain}}

@string{tlca93 = tlca # {, Utrecht, The Netherlands}}

@string{tlca97 = tlca # {, Nancy, France}}

@string{tlca99 = tlca # {, L'Aquila, Italy}}

@string{tldi = {ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI)}}

@string{tldi03 = tldi # {, New Orleans, Louisiana}}

@string{tocl = {ACM Transactions on Computational Logic}}

@string{toplas = {ACM Transactions on Programming Languages and Systems}}

@string{tose = {IEEE Transactions on Software Engineering}}

@string{tpa = {Workshop on Types for Program Analysis (TPA)} # informal}

@string{tr = {Tech. Report}}

@string{tsi = {Technique et Science Informatiques}}

@string{types = {International Workshop on Types for Proofs and Programs (TYPES)}}

@string{types93 = types # {, Nijmegen, The Netherlands}}

@string{types98 = types # {, Kloster Irsee, Germany}}

@string{u-lille = {Universit{\'e} des Sciences et Techniques de Lille    Flandres Artois}}

@string{univcaen = {Universit{\'e} de Caen}}

@string{univdenisdiderot = {Universit{\'e} Denis Diderot}}

@string{univnancy1 = {Universit{\'e} Henri Poincar{\'e} Nancy 1}}

@string{univparis7 = {Universit{\'e} Paris 7}}

@string{univparisnord = {Universit{\'e} Paris-Nord}}

@string{ups = {Universit{\'e} Paris-Sud}}

@string{ups-orsay = {Universit{\'e} Paris-Sud, Orsay, France}}

@string{wad79 = {Proc. 4th Workshop on Automated Deduction, Austin,    Texas}}

@string{webdb = {International Workshop on the Web and Databases (WebDB)}}

@string{xsym = {Database and XML Technologies: International XML Database Symposium (XSym)}}

@string{yes = {Yes}}


@unpublished{sozeau.Coq/lambda/notes,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Note = {Literate {C}oq script},
	Pdf = {http://mattam.org/research/publications/drafts/lambda-notes.pdf},
	Read = {Oui},
	Title = {A dependently-typed formalization of simply-typed lambda-calculus: substitution, denotation, normalization},
	Year = {2007}}

@misc{sozeau.Coq/FingerTrees/types07,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at TYPES'07},
	Location = {Cividale Del Friuli, Italy},
	Month = {2-5 May},
	Pdf = {http://mattam.org/research/publications/Program-ing_Finger_Trees_in_Coq-types07-040507.pdf},
	Read = {Oui},
	Title = {A journey with {R}ussell: {P}rogramming {D}ependent {F}inger {T}rees in {C}oq},
	Type = {slides},
	Year = {2007}}

@misc{sozeau.thesis-slides,
	Address = {Orsay, France},
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Thesis Defense},
	Month = {8th December},
	Read = {Oui},
	School = {Paris 11 University},
	Title = {{An Environment for Programming with Dependent Types}},
	Url = {http://mattam.org/research/publications/An_Environment_for_Programming_with_Dependent_Types-LRI-081208.pdf},
	Year = {2008},
	Bdsk-Url-1 = {http://mattam.org/research/publications/drafts/thesis-sozeau.pdf}}

@mastersthesis{sozeau.Coq/Russell/report,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Keywords = {coercion, subsets, Calculus of Constructions},
	Location = {LRI, Orsay},
	Pdf = {http://mattam.org/research/russell/report.pdf},
	Read = {Oui},
	School = {Universit\'e Paris VII},
	Title = {Coercion par pr\'edicats en {C}oq},
	Year = {2005}}

@unpublished{sozeau.Coq/dpm/equations,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Note = {Working version in french},
	Read = {Oui},
	Title = {Compilation du filtrage d{\'e}pendant},
	Url = {http://mattam.org/research/publications/drafts/Equations.pdf},
	Year = {2008},
	Bdsk-Url-1 = {http://mattam.org/research/publications/drafts/Equations.pdf}}

@inbook{sozeau.Coq/manual/Program,
	Author = {Matthieu Sozeau},
	Chapter = {Program},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Publisher = {INRIA TypiCal},
	Read = {Oui},
	Title = {Coq 8.2 Reference Manual},
	Url = {http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual027.html},
	Year = {2008},
	Bdsk-Url-1 = {http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual027.html}}

@inbook{sozeau.Coq/manual/typeclasses,
	Author = {Matthieu Sozeau},
	Chapter = {Type Classes},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Publisher = {INRIA TypiCal},
	Read = {Oui},
	Title = {Coq 8.2 Reference Manual},
	Url = {http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual024.html},
	Year = {2008},
	Bdsk-Url-1 = {http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual024.html}}

@inbook{sozeau.Coq/manual/setoid,
	Author = {Matthieu Sozeau},
	Chapter = {User defined equalities and relations},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Publisher = {INRIA TypiCal},
	Read = {Oui},
	Title = {Coq 8.2 Reference Manual},
	Url = {http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual029.html},
	Year = {2008},
	Bdsk-Url-1 = {http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual029.html}}

@misc{sozeau.Coq/FingerTrees/dtp08,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at DTP'08},
	Location = {Nottingham, UK},
	Month = {18--20 February},
	Pdf = {http://mattam.org/research/publications/Dependent_Finger_Trees-dtp08-180208.pdf},
	Read = {Oui},
	Title = {{D}ependent {F}inger {T}rees},
	Type = {slides},
	Year = {2008}}

@misc{sozeau.Coq/FingerTrees/web,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Read = {Oui},
	Title = {{D}ependent {F}inger {T}rees in {C}oq},
	Web = {http://mattam.org/research/russell/fingertrees.en.html},
	Year = {2007}}

@misc{sozeau.Coq/classes/Gallium08,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at the {G}allium seminar},
	Keywords = {Type classes},
	Location = {Rocquencourt},
	Month = {3rd November},
	Pdf = {http://mattam.org/research/publications/First-Class_Type_Classes-Gallium-031108.pdf},
	Read = {Oui},
	Title = {{F}irst-{C}lass {T}ype {C}lasses},
	Type = {slides},
	Year = {2008},
	Abstract = {Les classes de types ont d{\'e}montr{\'e} leur utilit{\'e} pour la programmation
polymorphique de haut-niveau en Haskell et la construction de
hi{\'e}rarchies de structures math{\'e}matiques dans l'assistant de preuve
Isabelle. Ce m{\'e}canisme de surcharge tr{\`e}s versatile peut se g{\'e}n{\'e}raliser
aux types d{\'e}pendants et offre alors de nouvelles formes de g{\'e}n{\'e}ricit{\'e}.
Il permet aussi d'int{\'e}grer une forme de programmation logique au moment
du typage.  On pr{\'e}sentera une impl{\'e}mentation l{\'e}g{\`e}re d'un syst{\`e}me de
classes de types de premi{\`e}re classe dans Coq, bas{\'e}e sur un
enrichissement de constructions existantes du langage Gallina. On
illustrera ce nouvel outil par des exemples mettant en oeuvre les
classes pour programmer, prouver et organiser les d{\'e}veloppements en Coq.
}}

@inproceedings{sozeau.Coq/classes/fctc,
	Author = {Matthieu Sozeau and Nicolas Oury},
	Booktitle = {Theorem Proving in Higher Order Logics, 21th International Conference},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Doi = {10.1007/978-3-540-71067-7_23},
	Editor = {Otmane Ait Mohamed, C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar},
	Keywords = {Type classes},
	Month = {August},
	Pages = {278-293},
	Pdf = {http://mattam.org/research/publications/First-Class_Type_Classes.pdf},
	Publisher = {Springer},
	Read = {Oui},
	Series = {Lecture Notes in Computer Science},
	Slides = {http://mattam.org/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf},
	Title = {{F}irst-{C}lass {T}ype {C}lasses},
	Volume = {5170},
	Year = {2008},
	Abstract = {
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for 
specifying with abstract structures by quantification on contexts. However, 
both systems are limited by second-class implementations of these constructs,
and these limitations are only overcomed by ad-hoc extensions to 
the respective systems. We propose an embedding of type classes into a 
dependent type theory that is first-class and supports some of the most 
popular extensions right away. The implementation is correspondingly 
cheap, general and very well integrated inside the system, as we have 
experimented in Coq. We show how it can be used to help structured 
programming and proving by way of examples.},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-71067-7_23}}

@misc{sozeau.Coq/classes/tphols08,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at {TPHOLs}'08},
	Keywords = {Type classes},
	Location = {Montr{\'e}al, Canada},
	Month = {20th August},
	Pdf = {http://mattam.org/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf},
	Read = {Oui},
	Title = {{F}irst-{C}lass {T}ype {C}lasses},
	Type = {slides},
	Year = {2008}}

@misc{sozeau.Coq/classes/proval08,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at the {P}ro{V}al workgroup},
	Keywords = {Type classes},
	Location = {Orsay},
	Month = {3rd March},
	Pdf = {http://mattam.org/research/publications/First-Class_Type_Classes-LRI-030308.pdf},
	Read = {Oui},
	Title = {{F}irst-{C}lass {T}ype {C}lasses, in {C}oq},
	Type = {slides},
	Year = {2008}}

@misc{sozeau.Coq/order,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Coq development},
	Read = {Oui},
	Title = {{O}rder theory using type classes in {C}oq},
	Web = {http://mattam.org/research/coq},
	Year = {2008}}

@inproceedings{sozeau.Coq/FingerTrees/article,
	Author = {Matthieu Sozeau},
	Booktitle = {ICFP'07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming},
	Copyright = {ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in    ICFP'07, http://doi.acm.org/10.1145/1291151.1291156},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Doi = {http://doi.acm.org/10.1145/1291151.1291156},
	Isbn = {978-1-59593-815-2},
	Location = {Freiburg, Germany},
	Pages = {13--24},
	Pdf = {http://mattam.org/research/publications/Program-ing_Finger_Trees_in_Coq.pdf},
	Publisher = {ACM Press},
	Read = {Oui},
	Slides = {http://mattam.org/research/publications/Program-ing_Finger_Trees_in_Coq-icfp07-011007.pdf},
	Title = {{P}rogram-ing {F}inger {T}rees in {C}oq},
	Year = {2007},
	Abstract = {Finger Trees (Hinze & Paterson, JFP 2006) are a general purpose persistent
data structure with good performance. Their genericity permits developing
a wealth of structures like ordered sequences or interval trees
on top of a single implementation. However, the type systems
used by current functional languages do not guarantee the coherent
parameterization and specialization of Finger Trees, let alone the
correctness of their implementation.
We present a certified implementation of Finger Trees solving
these problems using the {P}rogram extension of {C}oq. 
We not only implement the structure but also prove its
invariants along the way, which permit building certified
structures on top of Finger Trees in an elegant way.},
	Bdsk-Url-1 = {http://doi.acm.org/10.1145/1291151.1291156}}

@misc{sozeau.Coq/FingerTrees/icfp07,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at ICFP'07},
	Location = {Freiburg, Germany},
	Month = {1--3 October},
	Pdf = {http://mattam.org/research/publications/Program-ing_Finger_Trees_in_Coq-icfp07-011007.pdf},
	Read = {Oui},
	Title = {{P}rogram-ing {F}inger {T}rees in {C}oq},
	Type = {slides},
	Year = {2007}}

@misc{sozeau.Coq/Programing/proval07,
	Author = me,
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at the {P}ro{V}al seminar},
	Location = {Orsay},
	Month = {9th march},
	Pdf = {http://mattam.org/research/publications/Program-ing_in_Coq-proval-090307.pdf},
	Read = {Oui},
	Title = {{P}rogram-ing in {C}oq},
	Type = {slides},
	Year = {2007}}

@misc{sozeau.Coq/Programing/gallium07,
	Author = me,
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at the {G}allium seminar},
	Location = {Rocquencourt},
	Month = {16th march},
	Pdf = {http://mattam.org/research/publications/Program-ing_in_Coq-gallium-160307.pdf},
	Read = {Oui},
	Title = {{P}rogram-ing in {C}oq},
	Type = {slides},
	Year = {2007}}

@misc{sozeau.Coq/Programing/psu08,
	Author = me,
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at {P}ortland {S}tate {U}niversity},
	Location = {Portland, OR},
	Month = {16th january},
	Pdf = {http://mattam.org/research/publications/Program-ing_in_Coq-psu-160108.pdf},
	Read = {Oui},
	Title = {{P}rogram-ing in {C}oq},
	Type = {slides},
	Year = {2008}}

@misc{sozeau.Coq/Programing/harvard08,
	Author = me,
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at {H}arvard},
	Location = {Cambridge, MA},
	Month = {23th january},
	Pdf = {http://mattam.org/research/publications/Program-ing_in_Coq-harvard-230108.pdf},
	Read = {Oui},
	Title = {{P}rogram-ing in {C}oq},
	Type = {slides},
	Year = {2008}}

@misc{sozeau.Coq/Russell/web,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Read = {Oui},
	Title = {{R}ussell},
	Web = {http://mattam.org/research/russell.en.html},
	Year = {2006}}

@unpublished{sozeau.Coq/Russell/meta,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Note = {Notes},
	Pdf = {http://mattam.org/research/russell/metaproof.pdf},
	Read = {Oui},
	Title = {Russell {M}etatheoretic {S}tudy in {C}oq},
	Year = {2006}}

@misc{sozeau.Coq/Russell/meta-web,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Read = {Oui},
	Title = {{R}ussell {M}etatheoretic {S}tudy in {Coq}, experimental development},
	Web = {http://mattam.org/research/russell/meta.en.html},
	Year = {2006}}

@misc{sozeau.Coq/Russell/types06,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Howpublished = {Talk given at TYPES'06},
	Location = {University of Nottingham, UK},
	Month = {19-21 april},
	Pdf = {http://mattam.org/research/publications/Subset_Coercions_in_Coq-types06-210406.pdf},
	Read = {Oui},
	Title = {Subset {C}oercions in {Coq}},
	Type = {slides},
	Year = {2006}}

@inproceedings{sozeau.Coq/Russell/article,
	Author = {Matthieu Sozeau},
	Booktitle = {TYPES'06},
	Copyright = {Springer},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Doi = {http://dx.doi.org/10.1007/978-3-540-74464-1_16},
	Editors = {Thorsten Altenkirch and James Chapman and Conor McBride},
	Pages = {237--252},
	Pdf = {http://mattam.org/research/publications/Subset_Coercions_in_Coq.pdf},
	Publisher = {Springer},
	Read = {Oui},
	Series = {Lecture Notes in Computer Science},
	Slides = {http://mattam.org/research/publications/Subset_Coercions_in_Coq-types06-210406.pdf},
	Title = {Subset {C}oercions in {C}oq},
	Volume = {4502},
	Year = {2007},
	Abstract = {We propose a new language for writing programs with dependent
  types on top of the {C}oq proof assistant. This language permits
  to establish a phase distinction between writing and proving
  algorithms in the {C}oq environment.  Concretely, this means allowing
  to write algorithms as easily as in a practical functional programming
  language whilst giving them as rich a specification as desired and
  proving that the code meets the specification using the whole {C}oq
  proof apparatus. This is achieved by extending conversion to an
  equivalence which relates types and subsets based on them, a technique
  originating from the ``Predicate subtyping'' feature of PVS
  and following mathematical convention. The typing judgements can be
  translated to the Calculus of Inductive Constructions by means of an interpretation
  which inserts coercions at the appropriate places. These coercions can
  contain existential variables representing the propositional parts of
  the final term, corresponding to proof obligations (or PVS
  type-checking conditions). A prototype implementation of this process
  is integrated with the {C}oq environment.},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-74464-1_16}}

@misc{sozeau.Coq/classes/web,
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Read = {Oui},
	Title = {{T}ype classes in {C}oq},
	Web = {http://mattam.org/research/coq/classes.en.html},
	Year = {2008}}

@phdthesis{sozeau.thesis,
	Address = {Orsay, France},
	Author = {Matthieu Sozeau},
	Date-Added = {2008-12-14 16:11:14 +0100},
	Date-Modified = {2008-12-14 16:11:14 +0100},
	Month = {December},
	Read = {Oui},
	School = {Universit{\'e} Paris 11},
	Slides = {http://mattam.org/research/publications/An_Environment_for_Programming_with_Dependent_Types-LRI-081208.pdf},
	Title = {Un environnement pour la programmation avec types d{\'e}pendants},
	Url = {http://mattam.org/research/publications/thesis-sozeau.pdf},
	Year = {2008},
	Bdsk-Url-1 = {http://mattam.org/research/publications/drafts/thesis-sozeau.pdf}}

@comment{BibDesk Smart Groups{
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">
<array>
	<dict>
		<key>conditions</key>
		<array>
			<dict>
				<key>comparison</key>
				<integer>2</integer>
				<key>key</key>
				<string>Keywords</string>
				<key>value</key>
				<string>HTT</string>
				<key>version</key>
				<string>1</string>
			</dict>
			<dict>
				<key>comparison</key>
				<integer>2</integer>
				<key>key</key>
				<string>Keywords</string>
				<key>value</key>
				<string>Ynot</string>
				<key>version</key>
				<string>1</string>
			</dict>
		</array>
		<key>conjunction</key>
		<integer>1</integer>
		<key>group name</key>
		<string>HTT &amp; Ynot</string>
	</dict>
	<dict>
		<key>conditions</key>
		<array>
			<dict>
				<key>comparison</key>
				<integer>2</integer>
				<key>key</key>
				<string>Author</string>
				<key>value</key>
				<string>Matthieu Sozeau</string>
				<key>version</key>
				<string>1</string>
			</dict>
			<dict>
				<key>comparison</key>
				<integer>2</integer>
				<key>key</key>
				<string></string>
				<key>value</key>
				<string></string>
				<key>version</key>
				<string>1</string>
			</dict>
		</array>
		<key>conjunction</key>
		<integer>0</integer>
		<key>group name</key>
		<string>Matthieu Sozeau</string>
	</dict>
	<dict>
		<key>conditions</key>
		<array>
			<dict>
				<key>comparison</key>
				<integer>4</integer>
				<key>key</key>
				<string>BibTeX Type</string>
				<key>value</key>
				<string>proceedings</string>
				<key>version</key>
				<string>1</string>
			</dict>
		</array>
		<key>conjunction</key>
		<integer>0</integer>
		<key>group name</key>
		<string>Proceedings</string>
	</dict>
</array>
</plist>
}}

@comment{BibDesk URL Groups{
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">
<array>
	<dict>
		<key>URL</key>
		<string>http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib</string>
		<key>group name</key>
		<string>B. Pierce</string>
	</dict>
	<dict>
		<key>URL</key>
		<string>file://localhost/Users/mat/research/demons-biblio/demons.bib</string>
		<key>group name</key>
		<string>Démons</string>
	</dict>
	<dict>
		<key>URL</key>
		<string>file://localhost/Users/mat/research/demons-biblio/demons2.bib</string>
		<key>group name</key>
		<string>Démons2</string>
	</dict>
	<dict>
		<key>URL</key>
		<string>file://localhost/Users/mat/research/demons-biblio/demons3.bib</string>
		<key>group name</key>
		<string>Démons3</string>
	</dict>
	<dict>
		<key>URL</key>
		<string>http://pauillac.inria.fr/~fpottier/biblio/english.bib</string>
		<key>group name</key>
		<string>F. Pottier</string>
	</dict>
	<dict>
		<key>URL</key>
		<string>file://localhost/Users/mat/research/publication/bib/pvs.bib</string>
		<key>group name</key>
		<string>PVS</string>
	</dict>
</array>
</plist>
}}