Home

Claude Kirchner publication list Books and monographies

1. Vienna Austria March 25 31 2006 P BOROVANSKY C KIRCHNER H KIRCHNER P E MOREAU C RINGEIS SEN An Overview of ELAN In Proceedings of the second International Workshop on Rewriting Logic and Applications C Kirchner H Kirchner r d 15 http www elsevier nl locate entcs volume16 html Electronic Notes in Theoretical Computer Science Pont Mousson France September 1998 P BOROVANSKY C KIRCHNER H KIRCHNER P E MOREAU M VITTEK ELAN A logical framework based on computational systems In Proceed ings of the first international workshop on rewriting logic J Meseguer r d 4 Electronic Notes in Theoretical Computer Science Asilomar California September 1996 P BOROVANSK C KIRCHNER H KIRCHNER Controlling Rewriting by Rewriting In Proceedings of the first international workshop on rewriting logic J Meseguer r d 4 Electronic Notes in Theoretical Computer Science Asilomar California September 1996 P BOROVANSKY C KIRCHNER H KIRCHNER Rewriting as a Unified Specification Tool for Logic and Control The ELAN Language In Sec ond International Workshop on the Theory and Practice of Algebraic Specifi cations A Sellink r d Electronic Workshops in Computing eWiC web site http ewic springer co uk Springer Verlag Amsterdam September 1997 P BOROVANSKY C KIRCHNER H KIRCHNER Strategies and rewriting
2. Application to program derecursivation Rapport interne 81 R 056 Centre de Recherche en Informatique de Nancy 1981 C KIRCHNER H KIRCHNER Manuel d utilisation de Aidarbre un diteur d arbres Rapport interne 82 R 042 Centre de Recherche en Informatique de Nancy 1982 C KIRCHNER H KIRCHNER Unification dans les th ories quationnelles Rapport interne 83 R 011 Centre de Recherche en Informatique de Nancy 1983 C KIRCHNER H KIRCHNER Constrained Equational Reasoning for Com pletion Research report 89 R 222 Centre de Recherche en Informatique de Nancy 1989 Proceedings of UNIF 89 1989 C KIRCHNER H KIRCHNER Rewriting theory and applications Re search report 89 E 225 Centre de Recherche en Informatique de Nancy 1989 DEA lecture C KIRCHNER Z QIAN P K SINGH J STUBER Xemantics A semantics of XSLT in ELAN Rapport LORIA 2001 C KIRCHNER Etude comparative des formateurs MINT GROFF NROFF associes aux editeurs Emacs VI Emin Rapport de fin de contrat Rapport interne 85 R 091 Centre de Recherche en Informatique de Nancy 1985 F KLAY E DOMENJOUD C KIRCHNER V rification S mantique de Sp cifications M tallurgiques Rapport de fin de contrat Inria Lorraine amp Crin 1993 P R TY C KIRCHNER H KIRCHNER P LESCANNE An algorithm for uni fication based on narrowing R
3. 114 115 116 117 118 C KIRCHNER H KIRCHNER J MESEGUER Operational semantics of OBJ 3 In Proceedings of 15th International Colloquium on Automata Languages and Programming Lecture Notes in Computer Science 317 Springer Verlag pp 287 301 1988 C KIRCHNER H KIRCHNER M VITTEK Designing Constraint Logic Pro gramming Languages using Computational Systems In Proceedings of the 2nd CCL Workshop La Escala Spain F Orejas r d September 1993 C KIRCHNER H KIRCHNER M VITTEK Implementing Computational Systems with Constraints In Proceedings of the first Workshop on Princi ples and Practice of Constraint Programming Providence R I USA P Kanel lakis J L Lassez V Saraswat r d Brown University pp 166 175 1993 C KIRCHNER H KIRCHNER Trois m thodes de r solution d quations dans les alg bres libres et les vari t s quationnelles d alg bres In Actes des journ es GROPLAN GRECO Programmation Bergerac 1982 C KIRCHNER H KIRCHNER Nouvelles applications du syst me REVE In Actes du S minaire LITP 1984 C KIRCHNER H KIRCHNER Implementation of a general completion pro cedure parametrized by built in theories and strategies In Proceedings of the EUROCAL Conference Linz Austria B Buchberger r d Lecture Notes in Computer Science 204 Springer Verlag 19
4. ACM pp 250 261 January 2003 53 54 55 56 57 58 59 60 61 62 E BEFFARA O BOURNEZ H KACEM C KIRCHNER Verification of Timed Automata Using Rewrite Rules and Strategie In Seventh Biennial Bar Ilan Symposium on the Foundations of Artificial Intelligence BISFAI 01 Ramat Gan Israel June 2001 Also available as Technical Report A01 R 209 LORIA Nancy France C BERTOLISSI P BALDAN H CIRSTEA C KIRCHNER A rewriting cal culus for cyclic higher order term graphs In 2nd International Workshop on Term Graph Rewriting TERMGRAPH 2004 Rome Italy M Fernandez r d Electronic Notes in Theoretical Computer Science Oct 2004 C BERTOLISSI H CIRSTEA C KIRCHNER Translating Combinatory Re duction Systems into the Rewriting Calculus In 4th International Work shop on Rule Based Programming RULE 2008 Valencia Spain Jun 2003 Long version C BERTOLISSI C KIRCHNER The Rewriting Calculus as a Combinatory Reduction System In Prooceedings the FoSSaCS H Seidl r d LNCS Springer Verlag Braga Portugal mar 2007 F BLANQUI C KIRCHNER C RIBA On the Confluence of lambda Calculus with Conditional Rewriting In Proceedins of the 9th FoSSaCS Interna tional Conference L Aceto A Ing lfsd ttir r d Lecture Notes in Computer Science 3921 Springer Verlag pp 382 397
5. MEGRELIS Programming with equalities subsorts overloading and parameterization in OBJ Journal of Logic Programming 12 3 February 1992 pp 257 280 C KIRCHNER H KIRCHNER M RUSINOWITCH Deduction with symbolic constraints Revue d Intelligence Artificielle 4 3 1990 pp 9 52 Special issue on Automatic Deduction 41 42 43 44 C KIRCHNER H KIRCHNER REVEUR 3 Implementation of a General Completion Procedure Parametrized by Built in Theories and Strategies Science of Computer Programming 20 8 1986 pp 69 86 C KIRCHNER C RINGEISSEN Rule Based Constraint Programming Fundamenta Informaticae 34 3 September 1998 pp 225 262 C KIRCHNER L Action Concert Incitative S curit et Informatique Technique et Science Informatiques TSI 23 3 apr 2004 pp 421 426 Q H NGUYEN C KIRCHNER H KIRCHNER External rewriting for skep tical proof assistants extended version Journal of Automated Reasoning 29 3 4 2002 pp 309 336 Proceedings 45 46 47 48 49 50 51 52 M Api C KIRCHNER AC Unification Race the System Solving Ap proach In Proceedings of DISCO 90 A Miola r d Lecture Notes in Computer Science 429 Springer Verlag pp 174 183 Capri Italy April 1990 M ADI C KIRCHNER Associative Commutative Matching Based on the Syntact
6. Springer Verlag Miami Florida July 2003 E DEPLAGNE C KIRCHNER Deduction versus Computation the Case of Induction In Proceedings of the AISC and Calculemus conferences J Calmet B Benhamou O Caprotti L Henocque V Sorge r d Lecture Notes in Computer Science 2385 Springer Verlag pp 4 6 Marseille France July 2002 N DERSHOWITZ C KIRCHNER Inversion Strategies In Third Work shop on Rule Based Constraint Reasoning and Programming RCoRP 01 Paphos Cyprus December 2001 N DERSHOWITZ C KIRCHNER Abstract canonical inference systems In Proceedings of the UNIF 02 workshop July 2002 N DERSHOWITZ C KIRCHNER Abstract Saturation Based Inference In Proceedings of LICS P Kolaitis r d IEEE Ottawa Ontario June 2003 E DOMENJOUD C KIRCHNER J ZHOU Generating feasible schedules for a pick up and delivery problem In Proceedings of the CP98 work shop on Large Scale Combinatorial Optimisation and Constraints M Wal lace Y Caseau E Jacquet Lagreze H Simonis G Pesant r d Elsevier Electronic Notes in Discrete Mathematics volume 1 October 1998 textt thttp www elsevier nl locate disc D J DOUGHERTY C KIRCHNER H KIRCHNER A S DE OLIVEIRA Modular Access Control Via Strategic Rewriting In Computer Secu rity ESORICS 2007 12th European Symposium On Research In Compute
7. in ELAN In Proc of the CADE 14 workshop Strategies in Automated Deduction Townsville Australia 1997 Report CRIN 97 R 126 63 64 65 66 67 68 69 70 71 72 73 P BOROVANSKY C KIRCHNER H KIRCHNER A functional view of rewrit ing and strategies for a semantics of ELAN In The Third Fuji International Symposium on Functional and Logic Programming M Sato Y Toyama r d World Scientific pp 143 167 Kyoto April 1998 O BOURNEZ C KIRCHNER Probabilistic rewrite strategies Applications to ELAN In Proceedings of the RTA conference S Tison r d Lecture Notes in Computer Science Springer Verlag Copenhagen July 2002 P BRAUNER C HOUTMANN C KIRCHNER Principle of superdeduction In Proceedings of LICS L Ong r d pp 41 50 jul 2007 P BRAUNER C HOUTMANN C KIRCHNER Superdeduction at work In Rewriting Computation and Proof Essays Dedicated to Jean Pierre Jouan naud on the Occasion of His 60th Birthday H Comon C Kirchner H Kirchner r d 4600 Springer jun 2007 G BUREL C KIRCHNER Completion is an Instance of Abstract Canonical System Inference In Algebra Meaning and Computation Festschrift in Honor of Prof Joseph Goguen K Futatsugi J P Jouannaud J Meseguer r d Lecture Notes in Computer Science 4060 Springer Verlag pp 497 520
8. pp 47 103 N DERSHOWITZ C KIRCHNER Abstract canonical presentations The oretical Computer Science 357 1 3 July 2006 pp 53 69 N DoGGaz C KIRCHNER Completion for Unification Theoretical Computer Science 85 1 1991 pp 231 251 G DOWEK T HARDIN C KIRCHNER Higher order unification via explicit substitutions Information and Computation 157 1 2 2000 pp 183 235 G DOWEK T HARDIN C KIRCHNER HOL Ao an intentional first order expression of higher order logic Mathematical Structures in Computer Sci ence 11 1 2001 pp 21 45 G DOWEK T HARDIN C KIRCHNER Theorem Proving Modulo Jour nal of Automated Reasoning 31 1 2003 pp 33 72 I GNAEDIG C KIRCHNER H KIRCHNER Equational Completion in Order Sorted Algebras Theoretical Computer Science 72 1990 pp 169 202 J A GOGUEN C KIRCHNER S LEINWAND J MESEGUER T WINKLER Progress Report on the Rewrite Rule Machine IEEE Computer Architec ture Technical Commitee Newsletter Mars 1986 pp 7 21 M HERMANN C KIRCHNER H KIRCHNER Implementations of Term Rewriting Systems Computer Journal 34 1 1991 pp 20 33 C HINTERMEIER C KIRCHNER H KIRCHNER Dynamically Typed Com putations for Order Sorted Equational Presentations Journal of Symbolic Computation 25 4 1998 pp 455 526 J P JOUANNAUD C KIRCHNER H KIRCHNER A
9. r d Advances in Formal Methods 2 Kluwer Academic Publish ers Boston 2000 ch 6 pp 307 330 C KIRCHNER H KIRCHNER M VITTEK Designing Constraint Logic Pro gramming Languages using Computational Systems In Principles and Practice of Constraint Programming The Newport Papers P Van Hentenryck et V Saraswat r d The MIT press 1995 ch 8 pp 131 158 C KIRCHNER H KIRCHNER r d Automated Deduction CADE 15 Springer Verlag July 1998 C KIRCHNER H KIRCHNER r d Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications WRLA 98 Pont a Mousson France Electronic Notes in Theoretical Computer Science Septem ber 1998 C KIRCHNER From Unification in Combination of Equational Theories to a new AC unification algorithm In Resolution of Equations in Algebraic Structures Volume 2 Rewriting Techniques H Ait Kaci et M Nivat r d Academic Press New York 1989 ch 6 pp 171 210 C KIRCHNER r d Unification Academic Press London 1990 13 14 15 C KIRCHNER r d Proceedings 5th Conference on Rewriting Techniques and Applications Montreal Canada Springer Verlag June 1993 C KIRCHNER r d Special Issue on RTA 93 Theoretical Computer Science Elsevier Science Publishers B V North Holland 1995 C KIRCHNER r d Proceedings of the 4th International ACM SIGPLAN C
10. Notes in Theoretical Computer Science pp 3 19 Pisa Italy 2002 11 Internal publications and technical reports 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 P BOROVANSKY H CIRSTEA H DuBois C KIRCHNER H KIRCHNER P E MOREAU C RINGEISSEN M VITTEK ELAN V 3 3 User Manual dition third LORIA Nancy France December 1998 P BOROVANSK H CIRSTEA H DuBois C KIRCHNER H KIRCHNER P E MOREAU C RINGEISSEN M VITTEK ELAN V 3 4 User Manual dition fourth LORIA Nancy France January 2000 C CASTRO C KIRCHNER Towards a Methodology for Rule Based Pro gramming technical report LORIA December 2002 H CIRSTEA C KIRCHNER An introduction to the rewriting calculus Research Report RR 3818 INRIA December 1999 E DOMENJOUD C KIRCHNER J ZHOU Le manuel de ROUTER LORIA October 1998 E DOMENJOUD C KIRCHNER J ZHOU The ROUTER transport scheduling system Technical report LORIA October 1998 G DOWEK T HARDIN C KIRCHNER Higher order unification via ex plicit substitutions Rapport RR 2709 INRIA Lorraine November 1995 available under http www loria fr equipe protheo html G DOWEK T HARDIN C KIRCHNER HOL Ao an intentional first order expression of higher order logic Rapport de Recherche 3556 Institut N
11. 2 1 February 2001 pp 69 98 H CIRSTEA G FAURE C KIRCHNER A rho calculus of explicit constraint application ENTCS Proceedings of WRLA Workshop on Rewriting Logic and Applications Barcelona Spain March 2004 117 January 2005 pp 51 67 H CIRSTEA G FAURE C KIRCHNER A Rho Calculus of explicit constraint application Higher Order and Symbolic Computation To appear 20 2007 H CIRSTEA C KIRCHNER Rewriting and Multisets in Rho calculus and ELAN Romanian Journal of Information Science and Technology 4 1 2 2001 pp 33 48 ISSN 1453 8245 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 H CIRSTEA C KIRCHNER The Rewriting Calculus Part I Logic Journal of the Interest Group in Pure and Applied Logics 9 May 2001 pp 363 399 Also available as Technical Report A01 R 203 LORIA Nancy France H CIRSTEA C KIRCHNER The Rewriting Calculus Part II Logic Journal of the Interest Group in Pure and Applied Logics 9 May 2001 pp 401 434 Also available as Technical Report A01 R 204 LORIA Nancy France H Comon M DINCBAS J P JOUANNAUD C KIRCHNER A Method ological View of Constraint Solving Constraints 4 4 December 1999 pp 337 361 H Comon C KIRCHNER Constraint Solving on Terms Lecture Notes in Computer Science 2002 2001
12. 4 125 126 127 128 129 130 C KIRCHNER C LYNCH C SCHARFF A Fine grained Concurrent Com pletion Procedure In Proceedings of RTA 96 H Ganzinger r d Lecture Notes in Computer Science 1103 Springer Verlag pp 3 17 September 1996 C KIRCHNER P E MOREAU A REILLES Formal validation of pattern matching code In Barahona et Felty 2 pp 187 197 C KIRCHNER C RINGEISSEN Higher order equational unification via ex plicit substitutions In Proceedings of the tenth UNIF Workshop K U Schulz S Kepser r d Munich Germany June 1996 C KIRCHNER C RINGEISSEN Higher Order Equational Unification via Explicit Substitutions In Proceedings 6th International Joint Confer ence ALP HOA 97 Lecture Notes in Computer Science 1298 Springer Verlag pp 61 75 Southampton UK September 1997 C KIRCHNER P VIRY Implementing Parallel Rewriting In Paral lelization in Inference Systems B Fronh fer G Wrightson r d Lecture Notes in Artificial Intelligence 590 Springer Verlag pp 123 138 1992 C KIRCHNER A New Equational Unification Method A Generalization of Martelli Montanari Algorithm In Proceedings 7th International Conference on Automated Deduction Napa Valley Calif USA R Shostak r d Lecture Notes in Computer Science 170 Springer Verlag 1984 C KIRCHNER Co
13. 85 C KIRCHNER H KIRCHNER Constrained Equational Reasoning In Proceedings of the ACM SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation Portland Oregon ACM Press pp 382 389 July 1989 Report CRIN 89 R 220 C KIRCHNER H KIRCHNER Rule Based Programming and Proving The ELAN Experience Outcomes In Advances in Computer Science ASIAN 2004 Higher Level Decision Making 9th Asian Computing Science Conference Dedicated to Jean Louis Lassez on the Occasion of His 5th Cycle Birthday M J Maher r d Lecture Notes in Computer Science 3321 Springer pp 363 379 Chiang Mai Thailand December 8 10 2004 C KIRCHNER F KLAY A Note on Syntacticness In Proceedings 3rd International Workshop on Unification Lambrecht Germany H J Biirckert W Nutt r d June 1989 C KIRCHNER F KLAY Syntactic Theories and Unification In Pro ceedings 5th IEEE Symposium on Logic in Computer Science Philadelphia Pa USA pp 270 277 June 1990 C KIRCHNER R KOPETZ P E MOREAU Anti Pattern Matching In 16th European Symposium on Programming ESOP 07 Braga Portugal 2007 C KIRCHNER P LESCANNE Solving Disequations In Proceedings 2nd IEEE Symposium on Logic in Computer Science Ithaca N Y USA D Gries r d IEEE pp 347 352 1987 10 119 120 121 122 123 12
14. Claude Kirchner publication list Books and monographies 1 2 10 11 12 K APT C KIRCHNER r d Special Issue Foundations of Constraint Pro gramming Fundamenta Informaticae IOS Press 1998 P BARAHONA A P FELTY r d Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming July 11 13 2005 Lisbon Portugal ACM 2005 H CIRSTEA C KIRCHNER Combining Higher Order and First Order Com putation Using p calculus Towards a semantics of ELAN In Frontiers of Combining Systems 2 D Gabbay et M de Rijke r d Research Studies ISBN 0863802524 Wiley 1999 pp 95 120 H Comon C KIRCHNER H KIRCHNER r d Rewriting Computation and Proof Essays Dedicated to Jean Pierre Jouannaud on the Occasion of His 60th Birthday Springer jun 2007 M FERNANDEZ C KIRCHNER r d Proceedings of the first International Workshop on Security and Rewriting Techniques entcs 2006 J P JOUANNAUD C KIRCHNER Solving equations in abstract algebras a rule based survey of unification In Computational Logic Essays in honor of Alan Robinson J L Lassez et G Plotkin r d The MIT press Cambridge MA USA 1991 ch 8 pp 257 321 C KIRCHNER H KIRCHNER A MEGRELIS OBJ for OBJ In Soft ware Engineering with OBJ Algebraic Specification in Action J A Goguen et G Malcolm
15. KLER OBJ as a Lan guage for Concurrent Programming In Proceedings of Second International 97 98 99 100 101 102 103 104 105 106 Supercomputing Conference Volume I S Kartashev S Kartashev r d In ternational Supercomputing Institute Inc pp 195 198 Santa Clara CA USA 1987 J A GOGUEN C KIRCHNER J MESEGUER Concurrent Term Rewriting as a Model of Computation In Proceedings of Graph Reduction Workshop R Keller J Fasel r d Lecture Notes in Computer Science 279 Springer Verlag pp 53 93 Santa Fe NM USA 1987 C HINTERMEIER C KIRCHNER H KIRCHNER Strict Matchings and Uni fications in G algebras In Proceedings of the 9th WADT 4th Compass Workshop 1992 Centre de Recherche en Informatique de Nancy 92 R 268 C HINTERMEIER C KIRCHNER H KIRCHNER Dynamically Typed Com putations for Order Sorted Equational Presentations Extended Abstract In Proc 21st International Colloquium on Automata Languages and Pro gramming S Abiteboul E Shamir r d Lecture Notes in Computer Science 820 Springer Verlag pp 450 461 1994 C HINTERMEIER C KIRCHNER H KIRCHNER Order Sorted Completion with Dynamic Types In Proceedings of the 10th WADT 6th Compass Workshop May 1994 C HINTERMEIER C KIRCHNER H KIRCHNER Sort Inheritance for Order Sorted Equati
16. San Diego June 2006 G BUREL C KIRCHNER Cut Elimination in Deduction Modulo by Ab stract Completion In Proc of the Symposium on Logical Foundations of Computer Science S Artemov A Nerode r d Lecture Notes in Computer Science Springer Verlag New York USA jun 2007 C CASTRO C KIRCHNER Constraint Rewriting In Proceedings of The Workshop on Applications of Rewriting 9th International Conference on Rewriting Techniques and Applications RTA 98 Tsukuba Japan March 1998 C CASTRO C KIRCHNER Using Computational Systems as a General Framework for Handling CSPs In Proceedings of The Annual Work shop of The Constraints in Computational Logics Working Group CCL 98 Jerusalem Israel September 1998 H CIRSTEA C KIRCHNER L LIQUORI Matching Power In 12th In ternational Conference on Rewriting Techniques and Applications RTA 2001 A Middeldorp r d Lecture Notes in Computer Science 2051 Springer pp 77 92 Utrecht The Netherlands May 2001 Also available as Tech nical Report A01 R 201 LORIA Nancy France H CIRSTEA C KIRCHNER L LIQUORI The Rho Cube In 4th International Conference on Foundations of Software Science and Computation Structures FOSSACS 2001 F Honsell M Miculan r d Lecture Notes in Computer Science 2030 Springer pp 168 183 Genova Italy April 2001 Also available as Technic
17. a tional de Recherche en Informatique et en Automatique November 1998 G DOWEK T HARDIN C KIRCHNER Theorem Proving Modulo Rap port de Recherche 3400 Institut National de Recherche en Informatique et en Automatique April 1998 G DOWEK T HARDIN C KIRCHNER Theorem Proving Modulo revised version Rapport de Recherche 4861 Institut National de Recherche en Informatique et en Automatique July 2003 I GNAEDIG C KIRCHNER H KIRCHNER Equational Completion in Order sorted Algebras Rapport 87 R 086 Centre de Recherche en Informatique de Nancy 1987 J A GOGUEN C KIRCHNER J MESEGUER Models of computation for the rewrite rule machine Technical report 86 R 104 Centre de Recherche en Informatique de Nancy 1986 C KIRCHNER H KIRCHNER A MEGRELIS OBJ for OBJ Rapport 87 R 085 Centre de Recherche en Informatique de Nancy 1987 C KIRCHNER H KIRCHNER F NAHON Narrowing Based Inductive Proof Search Rapport LORIA 2006 C KIRCHNER H KIRCHNER M RUSINOWITCH Deduction with symbolic constraints Rapport 1858 INRIA 1990 12 146 147 148 149 150 151 152 153 154 155 C KIRCHNER H KIRCHNER M VITTEK ELAN V 1 17 User Manual Inria Lorraine amp Crin Nancy France November 1995 C KIRCHNER H KIRCHNER Solving equations in the signed trees theory
18. al Report A01 R 202 LORIA Nancy France H CIRSTEA C KIRCHNER The rewriting calculus as a semantics of ELAN In 4th Asian Computing Science Conference J Hsiang A Ohori r d Lecture Notes in Computer Science 1538 Springer Verlag pp 8 10 Manila The Philippines December 1998 74 75 76 77 78 79 80 81 82 83 84 H CIRSTEA C KIRCHNER Using Rewriting and Strategies for Describing the B Predicate Prover In Proceedings of the Workshop on Strategies in Automated Deduction CADE 15 Lindau Germany July 1998 H CIRSTEA C KIRCHNER Combining Higher Order and First Order Com putation Using Rho Calculus Towards a Semantics of ELAN In Fro CoS 98 Amsterdam 1999 H CIRSTEA C KIRCHNER The simply typed rewriting calculus In 3rd International Workshop on Rewriting Logic and its Applications WRLA2000 September 2000 A S DE OLIVEIRA E K WANG C KIRCHNER H KIRCHNER Weaving Rewrite Based Access Control Policies In Proceedings of 5th ACM Work shop on Formal Methods in Security Engineering From Specifications to Code ACM Press George Mason University USA nov 2007 E DEPLAGNE C KIRCHNER H KIRCHNER Q H NGUYEN Proof Search and Proof Check for Equational and Inductive Theorems In Proceedings of CADE 19 F Baader r d Lecture Notes in Computer Science
19. apport CRIN 86 R 131 Centre de Recherche en Informatique de Nancy 1986 Miscellaneous 156 157 158 159 F AJILI C CASTRO E DOMENJOUD C KIRCHNER Rapport de fin de pr tude du probl me d affectation des courses pour le GIHP Champagne Rapport de fin de contrat November 1996 C KIRCHNER H KIRCHNER Rewriting Solving Proving A preliminary version of a book available at 1999 C KIRCHNER Order sorted Equational Unification Presented at the fifth International Conference on Logic Programming Seattle USA August 1988 Also as rapport de recherche INRIA 954 Dec 88 C KIRCHNER Unifications Cours de DEA 1989 13 160 UNIF 87 Extended Abstracts of the First International Workshop on Unifica tion 1987 CRIN report 87 R 34 161 UNIF 88 Extended Abstracts of the 2nd International Workshop on Unifica tion 1988 CRIN report 89 R 38 14
20. ceedings of the LPAR conference M Baaz A Voronkov r d Lec ture Notes in Computer Science xx Springer Verlag p yy Tbilisi Georgia October 2002 M EL HABIB C KIRCHNER H KIRCHNER J Y MARION S MERZ The QSL platform at LORIA In First QPQ Workshop on Deductive Software Components Miami Floride Jun 2003 G FAURE C KIRCHNER Exceptions in the rewriting calculus In Proceedings of the RTA conference S Tison r d Lecture Notes in Computer Science Springer Verlag pp 66 82 Copenhagen July 2002 D FORTIN C KIRCHNER P STROGOVA Routing in Regular Networks Using Rewriting In Proceedings of the CADE international workshop on automated reasoning in algebra ARIA J Slaney r d pp 5 8 June 1994 I GNAEDIG C KIRCHNER H KIRCHNER Equational Completion in Order sorted Algebras In Proceedings of the 13th Colloquium on Trees in Algebra and Programming M Dauchet M Nivat r d Lecture Notes in Computer Science 299 Springer Verlag pp 165 184 1988 J A GOGUEN C KIRCHNER H KIRCHNER A MEGRELIS J MESEGUER T WINKLER An Introduction to OBJ 3 In Proceedings 1st Inter national Workshop on Conditional Term Rewriting Systems Orsay France J P Jouannaud S Kaplan r d Lecture Notes in Computer Science 308 Springer Verlag pp 258 263 July 1987 J A GOGUEN C KIRCHNER J MESEGUER T WIN
21. icity of the AC Theory In Proceedings 6th International Workshop on Unification Dagstuhl Germany F Baader J Siekmann W Snyder r d Dagstuhl seminar 1992 F AJILI C KIRCHNER Combining Unification and Built In Constraints In Proceedings of the tenth UNIF Workshop K U Schulz S Kepser r d Munich Germany June 1996 F AJILI C KIRCHNER A Modular Framework for the Combination of Sym bolic and Built In Constraints In Proceedings of Fourteenth International Conference on Logic Programming L Naish r d The MIT press pp 331 345 Leuven Belgium July 1997 I ALOUINI C KIRCHNER Toward the Concurrent Implementation of Com putational Systems In Proceedings of ALP 96 M Hanus r d Lecture Notes in Computer Science Springer Verlag pp 1 31 Aachen Germany September 1996 E BALLAND C KIRCHNER P E MOREAU A S DE OLIVEIRA Modular Formal Islands Embed Theory in your Practice In Proceedings of the Third Taiwanese French Conference on Information Technology LORIA INRIA march 2006 E BALLAND C KIRCHNER P E MOREAU Formal Islands In AMAST Kuressaare Estonia M Johnson V Vene r d LNCS 4019 Springer Verlag pp 51 65 July 2006 G BARTHE H CIRSTEA C KIRCHNER L LIQUORI Pure Patterns Type Systems In Principles of Programming Languages POPL2003 New Orleans USA
22. mputing unification algorithms In Proceedings 1st IEEE Symposium on Logic in Computer Science Cambridge Mass USA pp 206 216 1986 C KIRCHNER ELAN Mod lisation et preuve en calcul de r criture pr sentation invit e In Approches Formelles dans l Assistance au D veloppement de Logiciels Nancy France June 2001 Also available as Technical Report A01 R 242 LORIA Nancy France C KIRCHNER Strategic Rewriting In 4th International Workshop on Reduction Strategies in Rewriting and Programming WRS 2004 Aachen Germany Jun 2004 P R TY C KIRCHNER H KIRCHNER P LESCANNE Narrower A new algorithm for unification and its application to logic programming In Proceedings 1st Conference on Rewriting Techniques and Applications Dijon France J P Jouannaud r d Lecture Notes in Computer Science 202 Springer Verlag pp 141 157 1985 HORATIU CIRSTEA CLAUDE KIRCHNER LUIGI LIQUORI BENJAMIN WACK Rewrite Strategies in the Rewriting Calculus In Proceedings of the Third International Workshop on Reduction Strategies in Rewriting and Programming B Gramlich S Lucas r d 86 Elsevier Valencia Spain June 2003 HORATIU CIRSTEA CLAUDE KIRCHNER LUIGI LIQUORI Rewriting Calculus with out Types In Proceedings of the fourth workshop on rewriting logic and applications F Gadducci U Montanari r d 71 Electronic
23. onal Presentations In Recent Trends in Data Types Specifi cation Lecture Notes in Computer Science 906 Springer Verlag pp 319 335 1995 J P JOUANNAUD C KIRCHNER H KIRCHNER A MEGRELIS OBJ Pro gramming with equalities subsorts overloading and parameterization In Proceedings 1st International Workshop on Algebraic and Logic Programming 49 Akademie Verlag pp 41 52 November 1988 Report CRIN 88 R 148 J P JOUANNAUD C KIRCHNER H KIRCHNER M PICARD Les arbres sign s un cadre alg brique pour la r solution d quation dans les arbres In Proceedings of Congr s AFCET Informatique Nancy 1980 J P JOUANNAUD C KIRCHNER H KIRCHNER Incremental unification in equational theories In Proceedings of the Allerton conference Allerton USA 1982 J P JOUANNAUD C KIRCHNER H KIRCHNER Incremental Construc tion of Unification Algorithms in Equational Theories In Proceedings In ternational Colloquium on Automata Languages and Programming Barcelona Spain J Diaz r d Lecture Notes in Computer Science 154 Springer Verlag pp 361 373 1983 C KIRCHNER H KIRCHNER J P JOUANNAUD Algebraic manipulations as a unification and matching strategy for linear equations in signed binary trees In Proceedings of IJCAI 81 Vancouver Canada 1981 107 108 109 110 111 112 113
24. onference on Principles and Practice of Declarative Programming PPDP 02 Pittsburgh USA ACM Press October 2002 16 C KIRCHNER S curit Informatique Introduction Vuibert 2006 Thesis 17 C KIRCHNER H KIRCHNER R solution d quations dans les alg bres libres et 18 les vari t s quationnelles d alg bres Th se de Doctorat de Troisi me Cycle Universit Henri Poincar Nancy 1 1982 C KIRCHNER M thodes et outils de conception syst matique d algorithmes d unification dans les th ories quationnelles Th se de Doctorat d Etat Uni versit Henri Poincar Nancy 1 Nancy 21 juin 1985 Articles 19 20 21 22 23 24 25 M ADI C KIRCHNER AC Unification Race the System Solving Approach Implementation and Benchmarks Journal of Symbolic Computation 14 1 1992 pp 51 70 C BERTOLISSI H CIRSTEA C KIRCHNER Expressing combinatory reduc tion systems derivations in the rewriting calculus Higher Order and Symbolic Computation 19 4 dec 2006 pp 345 376 P BOROVANSKY C KIRCHNER H KIRCHNER P E MOREAU ELAN from a rewriting logic point of view Theoretical Computer Science 285 July 2002 pp 155 185 P BOROVANSK C KIRCHNER H KIRCHNER C RINGEISSEN Rewriting with strategies in ELAN a functional semantics International Journal of Foundations of Computer Science 1
25. r Security Dresden Germany September 24 26 2007 Proceedings J Biskup J Lopez r d Lecture Notes in Computer Science 4734 Springer pp 578 593 2007 85 86 87 88 89 90 91 92 93 94 95 96 G DOWEK T HARDIN C KIRCHNER F PFENNING Unification via Ex plicit Substitutions The Case of Higher Order Patterns In Proceedings of JICSLP 96 M Maher r d The MIT press Bonn Germany September 1996 G DOWEK T HARDIN C KIRCHNER Higher order unification via explicit substitutions Extended abstract In Proceedings of LICS 95 D Kozen r d pp 366 374 San Diego June 1995 G DOWEK T HARDIN C KIRCHNER HOL Ao an intentional first order expression of higher order logic In RTA 99 June 1999 G DOWEK T HARDIN C KIRCHNER HOL Ao an intentional first order expression of higher order logic In Proceedings of RTA 99 P Narendran M Rusinowitch r d Lecture Notes in Computer Science Springer Verlag June 1999 G DOWEK T HARDIN C KIRCHNER A completeness theorem for an ex tension of first order logic with binders In Proceedings of the IJCAR work shop on Mechanized Reasoning about Languages with Variable Binding R Crole S Ambler A Momigliano r d June 2001 G DOWEK T HARDIN C KIRCHNER Binding Logic proofs and models In Pro

Claude Kirchner publication list Books and monographies

Contents

Download Pdf Manuals

Related Search

Related Contents