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


%% Created for Matthieu Sozeau at 2010-01-04 12:00:26 +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ä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-à-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érieure de Lyon}}

@string{ensparis = {Ecole Normale Supé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é 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é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'École Normale Supérieure}}

@string{lifo = {Laboratoire d'Informatique Fondamentale d'Orlé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ü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à 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ü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é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ü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èse de Doctorat}}

@string{thesedoctorat = {Thèse de Doctorat}}

@string{theseh = {Thèse d'habilitation}}

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

@string{theselri = {Thèse de Doctorat, Université de Paris-Sud, France}}

@string{thesenancy = {Thèse de Doctorat, Université 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é des Sciences et Techniques de Lille Flandres Artois}}

@string{univcaen = {Université de Caen}}

@string{univdenisdiderot = {Université Denis Diderot}}

@string{univnancy1 = {Université Henri Poincaré Nancy 1}}

@string{univparis7 = {Université Paris 7}}

@string{univparisnord = {Université Paris-Nord}}

@string{ups = {Université Paris-Sud}}

@string{ups-orsay = {Université 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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +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,
	Address = {Cividale Del Friuli, Italy},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at TYPES'07},
	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}}

@article{sozeau.Coq/rewrite/JFR,
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Journal = {Journal of Formalized Reasoning},
	Keywords = {rewriting setoid typeclasses},
	Month = {December},
	Number = {1},
	Pages = {41-62},
	Pdf = {http://jfr.cib.unibo.it/article/view/1574/1077},
	Read = {Oui},
	Title = {{A New Look at Generalized Rewriting in Type Theory}},
	Volume = {2},
	Year = {2009},
	Abstract = {Rewriting is an essential tool for computer-based reasoning, both automated and assisted. 
It is so because rewriting is a general notion that permits to model a wide range of problems and 
provides means to effectively solve them. In a proof assistant, rewriting can be used to replace terms in 
arbitrary contexts, generalizing the usual equational reasoning to reasoning modulo arbitrary relations. 
This can be done provided the necessary proofs that functions appearing in goals are congruent with 
respect to specific relations. We present a new implementation of generalized rewriting in the Coq proof 
assistant, making essential use of the expressive power of dependent types and a recently implemented 
type class mechanism. The tactic improves on and generalizes previous versions by supporting natively 
higher-order functions, polymorphism and subrelations. The type class system inspired from Haskell 
provides a perfect interface between the user and such tactics, making them easily extensible.}}

@misc{sozeau.Coq/rewrite/types09,
	Address = {Aussois, France},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {TYPES'09},
	Keywords = {rewriting setoid typeclasses},
	Month = {May},
	Pdf = {http://mattam.org/research/publications/A_New_Look_at_Generalized_Rewriting_in_Type_Theory-TYPES09-130509.pdf},
	Read = {Oui},
	Title = {{A New Look at Generalized Rewriting in Type Theory}},
	Type = {slides},
	Year = {2009},
	Abstract = {Rewriting is an essential tool for computer-based reasoning, both automated and assisted. 
It is so because rewriting is a general notion that permits to model a wide range of problems and 
provides means to effectively solve them. In a proof assistant, rewriting can be used to replace terms in 
arbitrary contexts, generalizing the usual equational reasoning to reasoning modulo arbitrary relations. 
This can be done provided the necessary proofs that functions appearing in goals are congruent with 
respect to specific relations. We present a new implementation of generalized rewriting in the Coq proof 
assistant, making essential use of the expressive power of dependent types and a recently implemented 
type class mechanism. The tactic improves on and generalizes previous versions by supporting natively 
higher-order functions, polymorphism and subrelations. The type class system inspired from Haskell 
provides a perfect interface between the user and such tactics, making them easily extensible.},
	Bdsk-Url-1 = {http://mattam.org/research/publications/drafts/Equations.pdf}}

@misc{sozeau.Coq/rewrite/coq09,
	Address = {Munich, Germany},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at the First Coq Workshop},
	Keywords = {rewriting setoid typeclasses},
	Month = {August},
	Pdf = {http://mattam.org/research/publications/A_New_Look_at_Generalized_Rewriting_in_Type_Theory-Coq09-210809.pdf},
	Read = {Oui},
	Title = {{A New Look at Generalized Rewriting in Type Theory}},
	Type = {slides},
	Year = {2009},
	Abstract = {Rewriting is an essential tool for computer-based reasoning, both automated and assisted. 
It is so because rewriting is a general notion that permits to model a wide range of problems and 
provides means to effectively solve them. In a proof assistant, rewriting can be used to replace terms in 
arbitrary contexts, generalizing the usual equational reasoning to reasoning modulo arbitrary relations. 
This can be done provided the necessary proofs that functions appearing in goals are congruent with 
respect to specific relations. We present a new implementation of generalized rewriting in the Coq proof 
assistant, making essential use of the expressive power of dependent types and a recently implemented 
type class mechanism. The tactic improves on and generalizes previous versions by supporting natively 
higher-order functions, polymorphism and subrelations. The type class system inspired from Haskell 
provides a perfect interface between the user and such tactics, making them easily extensible.},
	Bdsk-Url-1 = {http://mattam.org/research/publications/drafts/Equations.pdf}}

@article{sozeau.Coq/rewrite/newlook,
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Journal = {1st Coq Workshop proceedings},
	Keywords = {rewriting setoid typeclasses},
	Month = {August},
	Pdf = {http://mattam.org/research/publications/A_New_Look_at_Generalized_Rewriting_in_Type_Theory.pdf},
	Read = {Oui},
	Slides = {http://mattam.org/research/publications/A_New_Look_at_Generalized_Rewriting_in_Type_Theory-Coq09-210809.pdf},
	Title = {{A New Look at Generalized Rewriting in Type Theory}},
	Year = {2009},
	Abstract = {Rewriting is an essential tool for computer-based reasoning, both automated and assisted. 
It is so because rewriting is a general notion that permits to model a wide range of problems and 
provides means to effectively solve them. In a proof assistant, rewriting can be used to replace terms in 
arbitrary contexts, generalizing the usual equational reasoning to reasoning modulo arbitrary relations. 
This can be done provided the necessary proofs that functions appearing in goals are congruent with 
respect to specific relations. We present a new implementation of generalized rewriting in the Coq proof 
assistant, making essential use of the expressive power of dependent types and a recently implemented 
type class mechanism. The tactic improves on and generalizes previous versions by supporting natively 
higher-order functions, polymorphism and subrelations. The type class system inspired from Haskell 
provides a perfect interface between the user and such tactics, making them easily extensible.},
	Bdsk-Url-1 = {http://mattam.org/research/publications/drafts/Equations.pdf}}

@misc{sozeau.Coq/Programing/Nijmegen09,
	Address = {Nijmegen, Netherlands},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {ICIS Seminar},
	Month = {20th January},
	Pdf = {http://mattam.org/research/publications/An_Environment_for_Programming_with_Dependent_Types-Nijmegen-200109.pdf},
	Read = {Oui},
	Title = {{An Environment for Programming with Dependent Types}},
	Type = {slides},
	Year = {2009}}

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

@misc{sozeau.Coq/Programing/Orleans09,
	Address = {Orléans, France},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {LIFO Seminar},
	Month = {26th January},
	Pdf = {http://mattam.org/research/publications/An_Environment_for_Proving_and_Programming-LIFO-260109.pdf},
	Read = {Oui},
	Title = {{An Environment for Proving and Programming}},
	Type = {slides},
	Year = {2009}}

@inproceedings{sozeau.Coq/classes/ctpc,
	Address = {Toulouse, France},
	Author = {Matthieu Sozeau and Nicolas Oury},
	Booktitle = {Journées Nationales du GDR GPL},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Keywords = {Type classes},
	Month = {January},
	Pdf = {http://mattam.org/research/publications/Classes_de_types_de_premiere_classe.pdf},
	Read = {Oui},
	Slides = {http://mattam.org/research/publications/First-Class_Type_Classes-GDR_GPL-300109.pdf},
	Title = {{Classes de types de première classe}},
	Year = {2009},
	Abstract = {Les classes de types (Type Classes) ont remporté un grand
succès dans le langage de programmation fonctionnelle Haskell et
l'assistant de preuve Isabelle, comme solution permettant de
surcharger des notations et spécifier avec des structures
abstraites en quantifiant sur les contextes. Nous présentons un
plongement superficiel des classes de types dans une théorie des types
dépendants qui fait des classes des objets de première classe et
supporte directement les extensions les plus populaires de Haskell.
L'implémentation du système est légère et s'appuie sur des
constructions existantes du langage qui sont simplement raffinées pour
obtenir un ensemble bien intégré à l'environnement Coq. On
présente sur des exemples comment ce système peut être utilisé pour 
la programmation et la preuve.
},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-71067-7_23}}

@mastersthesis{sozeau.Coq/Russell/report,
	Address = {LRI, Orsay},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Keywords = {coercion, subsets, Calculus of Constructions},
	Pdf = {http://mattam.org/research/publications/master-sozeau.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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Note = {Working version in french},
	Pdf = {http://mattam.org/research/publications/drafts/Equations.pdf},
	Read = {Oui},
	Title = {Compilation du filtrage dépendant},
	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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Publisher = {INRIA TypiCal},
	Read = {Oui},
	Title = {Coq 8.2 Reference Manual},
	Url = {http://coq.inria.fr/V8.2rc2/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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Publisher = {INRIA TypiCal},
	Read = {Oui},
	Title = {Coq 8.2 Reference Manual},
	Url = {http://coq.inria.fr/V8.2rc2/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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Publisher = {INRIA TypiCal},
	Read = {Oui},
	Title = {Coq 8.2 Reference Manual},
	Url = {http://coq.inria.fr/V8.2rc2/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,
	Address = {Nottingham, UK},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at DTP'08},
	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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +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/GDRGPL09,
	Address = {ENSEEIHT - Toulouse},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at the {GDR GPL}},
	Keywords = {Type classes},
	Month = {30th January},
	Pdf = {http://mattam.org/research/publications/First-Class_Type_Classes-GDR_GPL-300109.pdf},
	Read = {Oui},
	Title = {{F}irst-{C}lass {T}ype {C}lasses},
	Type = {slides},
	Year = {2009},
	Abstract = {Les classes de types ont démontré leur utilité pour la programmation
polymorphique de haut-niveau en Haskell et la construction de
hiérarchies de structures mathématiques dans l'assistant de preuve
Isabelle. Ce mécanisme de surcharge très versatile peut se généraliser
aux types dépendants et offre alors de nouvelles formes de généricité.
Il permet aussi d'intégrer une forme de programmation logique au moment
du typage.  On présentera une implémentation légère d'un système de
classes de types de première classe dans Coq, basé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éveloppements en Coq.
}}

@misc{sozeau.Coq/classes/Gallium08,
	Address = {Rocquencourt},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at the {G}allium seminar},
	Keywords = {Type classes},
	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émontré leur utilité pour la programmation
polymorphique de haut-niveau en Haskell et la construction de
hiérarchies de structures mathématiques dans l'assistant de preuve
Isabelle. Ce mécanisme de surcharge très versatile peut se généraliser
aux types dépendants et offre alors de nouvelles formes de généricité.
Il permet aussi d'intégrer une forme de programmation logique au moment
du typage.  On présentera une implémentation légère d'un système de
classes de types de première classe dans Coq, basé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éveloppements en Coq.
}}

@inproceedings{sozeau.Coq/classes/fctc,
	Author = {Matthieu Sozeau and Nicolas Oury},
	Booktitle = {Theorem Proving in Higher Order Logics, 21th International Conference},
	Copyright = {Springer},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Doi = {10.1007/978-3-540-71067-7_23},
	Editor = {Otmane Ait Mohamed, César Muñoz and Sofiè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,
	Address = {Montréal, Canada},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at {TPHOLs}'08},
	Keywords = {Type classes},
	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,
	Address = {Orsay},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at the {P}ro{V}al workgroup},
	Keywords = {Type classes},
	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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +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,
	Address = {Freiburg, Germany},
	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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Doi = {http://doi.acm.org/10.1145/1291151.1291156},
	Isbn = {978-1-59593-815-2},
	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,
	Address = {Freiburg, Germany},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at ICFP'07},
	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/nottingham08,
	Address = {Nottingham, UK},
	Author = me,
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at the {F}oundations of {P}rogramming seminar},
	Month = {15th February},
	Pdf = {http://mattam.org/research/publications/Program-ing_in_Coq-nottingham-150208.pdf},
	Read = {Oui},
	Title = {{P}rogram-ing in {C}oq},
	Type = {slides},
	Year = {2008}}

@misc{sozeau.Coq/Programing/proval07,
	Address = {Orsay},
	Author = me,
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at the {P}ro{V}al seminar},
	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,
	Address = {Rocquencourt},
	Author = me,
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at the {G}allium seminar},
	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,
	Address = {Portland, OR},
	Author = me,
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at {P}ortland {S}tate {U}niversity},
	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,
	Address = {Cambridge, MA},
	Author = me,
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at {H}arvard},
	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/Programing/PPS09,
	Address = {Paris, France},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {PPS Seminar},
	Keywords = {dependent types, Coq, Program},
	Month = {26th February},
	Pdf = {http://mattam.org/research/publications/Programming_with_Dependent_Types_in_Coq-PPS-260209.pdf},
	Read = {Oui},
	Title = {{Programming with Dependent Types in Coq}},
	Type = {slides},
	Year = {2009}}

@misc{sozeau.Coq/Russell/web,
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +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,
	Address = {University of Nottingham, UK},
	Author = {Matthieu Sozeau},
	Date-Added = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Howpublished = {Talk given at TYPES'06},
	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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Doi = {http://dx.doi.org/10.1007/978-3-540-74464-1_16},
	Editor = {Thorsten Altenkirch 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 Coercions in Coq}},
	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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +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 = {2010-01-04 12:00:08 +0100},
	Date-Modified = {2010-01-04 12:00:08 +0100},
	Month = {December},
	Pdf = {http://mattam.org/research/publications/thesis-sozeau.pdf},
	Read = {Oui},
	School = {Université 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épendants},
	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>
}}