Download Claude Kirchner publication list Books and monographies

Claude Kirchner publication list
Books and monographies
[1] K. Apt, C. Kirchner (réd.). – Special Issue: Foundations of Constraint Programming, Fundamenta Informaticae. IOS Press, 1998.
[2] 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.
[3] H. Cirstea, C. Kirchner. – hh Combining Higher-Order and First-Order Computation Using ρ-calculus: Towards a semantics of ELAN ii. – In : Frontiers of
Combining Systems 2 , D. Gabbay et M. de Rijke (réd.), Research Studies, ISBN
0863802524 . Wiley, 1999, pp. 95–120.
[4] 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.
[5] M. Fernandez, C. Kirchner (réd.). – Proceedings of the first International
Workshop on Security and Rewriting Techniques. – entcs, 2006.
[6] J.-P. Jouannaud, C. Kirchner. – hh Solving equations in abstract algebras: a
rule-based survey of unification ii. – 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.
[7] C. Kirchner, H. Kirchner, A. Mégrelis. – hh OBJ for OBJ ii. – In : Software Engineering with OBJ: Algebraic Specification in Action, J. A. Goguen et
G. Malcolm (réd.), Advances in Formal Methods, 2 . Kluwer Academic Publishers, Boston, 2000, ch. 6, pp. 307–330.
[8] C. Kirchner, H. Kirchner, M. Vittek. – hh Designing Constraint Logic Programming Languages using Computational Systems ii. – 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.
[9] C. Kirchner, H. Kirchner (réd.). – Automated Deduction – CADE-15 . –
Springer-Verlag, July 1998.
[10] C. Kirchner, H. Kirchner (réd.). – Proceedings of the 2nd International
Workshop on Rewriting Logic and its Applications, WRLA’98 . – Pont-àMousson (France), Electronic Notes in Theoretical Computer Science, September 1998.
[11] C. Kirchner. – hh From Unification in Combination of Equational Theories to
a new AC-unification algorithm ii. – In : Resolution of Equations in Algebraic
Structures, Volume 2: Rewriting Techniques, H. Aı̈t-Kaci et M. Nivat (réd.).
Academic Press, New York, 1989, ch. 6, pp. 171–210.
[12] C. Kirchner (réd.). – Unification. Academic Press, London, 1990.
1
[13] C. Kirchner (réd.). – Proceedings 5th Conference on Rewriting Techniques and
Applications, Montreal (Canada). – Springer-Verlag, June 1993.
[14] C. Kirchner (réd.). – Special Issue on RTA-93 , Theoretical Computer Science.
Elsevier Science Publishers B. V. (North-Holland), 1995.
[15] C. Kirchner (réd.). – Proceedings of the 4th International ACM SIGPLAN
Conference 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
les variétés équationnelles d’algèbres. – Thèse de Doctorat de Troisième Cycle,
Université Henri Poincaré – Nancy 1, 1982.
[18] 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, Université Henri Poincaré – Nancy 1, Nancy, 21 juin 1985.
Articles
[19] M. Adi, C. Kirchner. – hh AC-Unification Race: the System Solving Approach,
Implementation and Benchmarks ii. – Journal of Symbolic Computation 14 , 1
(1992), pp. 51–70.
[20] C. Bertolissi, H. Cirstea, C. Kirchner. – hh Expressing combinatory reduction systems derivations in the rewriting calculus ii. – Higher-Order and Symbolic
Computation 19 , 4 (dec 2006), pp. 345–376.
[21] P. Borovansky, C. Kirchner, H. Kirchner, P.-E. Moreau. – hh ELAN
from a rewriting logic point of view ii. – Theoretical Computer Science, 285
(July 2002), pp. 155–185.
[22] P. Borovanský, C. Kirchner, H. Kirchner, C. Ringeissen. – hh Rewriting
with strategies in ELAN: a functional semantics ii. – International Journal of
Foundations of Computer Science 12 , 1 (February 2001), pp. 69–98.
[23] H. Cirstea, G. Faure, C. Kirchner. – hh A rho-calculus of explicit constraint
application ii. – ENTCS – Proceedings of WRLA (Workshop on Rewriting Logic
and Applications, Barcelona, Spain. March 2004) 117 (January 2005), pp. 51–
67.
[24] H. Cirstea, G. Faure, C. Kirchner. – hh A Rho-Calculus of explicit constraint
application ii. – Higher-Order and Symbolic Computation (To appear) 20 (2007).
[25] H. Cirstea, C. Kirchner. – hh Rewriting and Multisets in Rho-calculus and
ELAN ii. – Romanian Journal of Information, Science and Technology 4 , 1-2
(2001), pp. 33–48. – ISSN: 1453-8245.
2
[26] H. Cirstea, C. Kirchner. – hh The Rewriting Calculus - Part I ii. – 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).
[27] H. Cirstea, C. Kirchner. – hh The Rewriting Calculus - Part II 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).
[28] H. Comon, M. Dincbas, J.-P. Jouannaud, C. Kirchner. – hh A Methodological View of Constraint Solving ii. – Constraints 4 , 4 (December 1999),
pp. 337–361.
[29] H. Comon, C. Kirchner. – hh Constraint Solving on Terms ii. – Lecture Notes
in Computer Science 2002 (2001), pp. 47–103.
[30] N. Dershowitz, C. Kirchner. – hh Abstract canonical presentations ii. – Theoretical Computer Science 357 , 1-3 (July 2006), pp. 53–69.
[31] N. Doggaz, C. Kirchner. – hh Completion for Unification ii. – Theoretical
Computer Science 85 , 1 (1991), pp. 231–251.
[32] G. Dowek, T. Hardin, C. Kirchner. – hh Higher-order unification via explicit
substitutions ii. – Information and Computation 157 , 1/2 (2000), pp. 183–235.
[33] G. Dowek, T. Hardin, C. Kirchner. – hh HOL-λσ an intentional first-order
expression of higher-order logic ii. – Mathematical Structures in Computer Science 11 , 1 (2001), pp. 21–45.
[34] G. Dowek, T. Hardin, C. Kirchner. – hh Theorem Proving Modulo ii. – Journal of Automated Reasoning 31 , 1 (2003), pp. 33–72.
[35] I. Gnaedig, C. Kirchner, H. Kirchner. – hh Equational Completion in OrderSorted Algebras ii. – Theoretical Computer Science 72 (1990), pp. 169–202.
[36] J. A. Goguen, C. Kirchner, S. Leinwand, J. Meseguer, T. Winkler. –
hh Progress Report on the Rewrite Rule Machine ii. – IEEE Computer Architecture Technical Commitee Newsletter (Mars 1986), pp. 7–21.
[37] M. Hermann, C. Kirchner, H. Kirchner. – hh Implementations of Term
Rewriting Systems ii. – Computer Journal 34 , 1 (1991), pp. 20–33.
[38] C. Hintermeier, C. Kirchner, H. Kirchner. – hh Dynamically-Typed Computations for Order-Sorted Equational Presentations ii. – Journal of Symbolic
Computation 25 , 4 (1998), pp. 455–526.
[39] J.-P. Jouannaud, C. Kirchner, H. Kirchner, A. Mégrelis. –
hh Programming with equalities, subsorts, overloading and parameterization in
OBJ ii. – Journal of Logic Programming 12 , 3 (February 1992), pp. 257–280.
[40] C. Kirchner, H. Kirchner, M. Rusinowitch. – hh Deduction with symbolic
constraints ii. – Revue d’Intelligence Artificielle 4 , 3 (1990), pp. 9–52. – Special
issue on Automatic Deduction.
3
[41] C. Kirchner, H. Kirchner. – hh REVEUR-3: Implementation of a General
Completion Procedure Parametrized by Built-in Theories and Strategies ii. –
Science of Computer Programming 20 , 8 (1986), pp. 69–86.
[42] C. Kirchner, C. Ringeissen. – hh Rule-Based Constraint Programming ii. –
Fundamenta Informaticae 34 , 3 (September 1998), pp. 225–262.
[43] C. Kirchner. – hh L’Action Concerté Incitative Sécurité et Informatique ii. –
Technique et Science Informatiques - TSI 23 , 3 (apr 2004), pp. 421–426.
[44] Q.-H. Nguyen, C. Kirchner, H. Kirchner. – hh External rewriting for skeptical proof assistants (extended version) ii. – Journal of Automated Reasoning
29 , 3-4 (2002), pp. 309–336.
Proceedings
[45] M. Adi, C. Kirchner. – hh AC-Unification Race: the System Solving Approach ii. – In : Proceedings of DISCO’90 , A. Miola (réd.), Lecture Notes in
Computer Science, 429 , Springer-Verlag, pp. 174–183. – Capri (Italy), April
1990.
[46] M. Adi, C. Kirchner. – hh Associative Commutative Matching Based on the
Syntacticity of the AC Theory ii. – In : Proceedings 6th International Workshop
on Unification, Dagstuhl (Germany), F. Baader, J. Siekmann, W. Snyder (réd.),
Dagstuhl seminar. – 1992.
[47] F. Ajili, C. Kirchner. – hh Combining Unification and Built-In Constraints ii.
– In : Proceedings of the tenth UNIF Workshop, K. U. Schulz, S. Kepser (réd.).
– Munich, Germany, June 1996.
[48] F. Ajili, C. Kirchner. – hh A Modular Framework for the Combination of Symbolic and Built-In Constraints ii. – In : Proceedings of Fourteenth International
Conference on Logic Programming, L. Naish (réd.), The MIT press, pp. 331–345.
– Leuven, Belgium, July 1997.
[49] I. Alouini, C. Kirchner. – hh Toward the Concurrent Implementation of Computational Systems ii. – In : Proceedings of ALP’96 , M. Hanus (réd.), Lecture
Notes in Computer Science, Springer-Verlag, pp. 1–31. – Aachen (Germany),
September 1996.
[50] E. Balland, C. Kirchner, P.-E. Moreau, A. S. de Oliveira. – hh Modular
Formal Islands: Embed Theory in your Practice ii. – In : Proceedings of the Third
Taiwanese-French Conference on Information Technology, LORIA, INRIA. –
march 2006.
[51] E. Balland, C. Kirchner, P.-E. Moreau. – hh Formal Islands ii. – In :
AMAST, Kuressaare (Estonia), M. Johnson, V. Vene (réd.), LNCS , 4019 ,
Springer-Verlag, pp. 51–65. – July 2006.
[52] G. Barthe, H. Cirstea, C. Kirchner, L. Liquori. – hh Pure Patterns Type
Systems ii. – In : Principles of Programming Languages - POPL2003, New
Orleans, USA, ACM, pp. 250–261. – January 2003.
4
[53] E. Beffara, O. Bournez, H. Kacem, C. Kirchner. – hh Verification of Timed
Automata Using Rewrite Rules and Strategie ii. – In : Seventh Biennial Bar-Ilan
Symposium on the Foundations of Artificial Intelligence (BISFAI’01). – RamatGan (Israel), June 2001. Also available as Technical Report A01-R-209, LORIA,
Nancy (France).
[54] C. Bertolissi, P. Baldan, H. Cirstea, C. Kirchner. – hh A rewriting calculus for cyclic higher-order term graphs ii. – In : 2nd International Workshop
on Term Graph Rewriting - TERMGRAPH’2004, Rome, Italy, M. Fernandez
(réd.), Electronic Notes in Theoretical Computer Science. – Oct 2004.
[55] C. Bertolissi, H. Cirstea, C. Kirchner. – hh Translating Combinatory Reduction Systems into the Rewriting Calculus ii. – In : 4th International Workshop on Rule-Based Programming (RULE 2003), Valencia, Spain. – Jun 2003.
Long version.
[56] C. Bertolissi, C. Kirchner. – hh The Rewriting Calculus as a Combinatory
Reduction System ii. – In : Prooceedings the FoSSaCS , H. Seidl (réd.), LNCS ,
Springer-Verlag. – Braga, Portugal, mar 2007.
[57] F. Blanqui, C. Kirchner, C. Riba. – hh On the Confluence of lambda -Calculus
with Conditional Rewriting ii. – In : Proceedins of the 9th FoSSaCS International Conference, L. Aceto, A. Ingólfsdóttir (réd.), Lecture Notes in Computer
Science, 3921 , Springer-Verlag, pp. 382–397. – Vienna, Austria, March 25-31,
2006.
[58] P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen. – hh An Overview of ELAN ii. – 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.
[59] P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, M. Vittek. –
hh ELAN: A logical framework based on computational systems ii. – 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.
[60] P. Borovanský, C. Kirchner, H. Kirchner. – hh Controlling Rewriting by
Rewriting ii. – 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.
[61] P. Borovanský, C. Kirchner, H. Kirchner. – hh Rewriting as a Unified
Specification Tool for Logic and Control:The ELAN Language ii. – In : Second International Workshop on the Theory and Practice of Algebraic Specifications, A. Sellink (réd.), Electronic Workshops in Computing, eWiC web site:
http://ewic.springer.co.uk/ , Springer-Verlag. – Amsterdam, September 1997.
[62] P. Borovansky, C. Kirchner, H. Kirchner. – hh Strategies and rewriting
in ELAN ii. – In : Proc. of the CADE-14 workshop: Strategies in Automated
Deduction. – Townsville, Australia, 1997. Report CRIN 97-R-126.
5
[63] P. Borovanský, C. Kirchner, H. Kirchner. – hh A functional view of rewriting and strategies for a semantics of ELAN ii. – 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.
[64] O. Bournez, C. Kirchner. – hh Probabilistic rewrite strategies. Applications
to ELAN ii. – In : Proceedings of the RTA conference, S. Tison (réd.), Lecture
Notes in Computer Science, Springer-Verlag. – Copenhagen, July 2002.
[65] P. Brauner, C. Houtmann, C. Kirchner. – hh Principle of superdeduction ii.
– In : Proceedings of LICS , L. Ong (réd.), pp. 41–50. – jul 2007.
[66] P. Brauner, C. Houtmann, C. Kirchner. – hh Superdeduction at work ii. –
In : Rewriting, Computation and Proof. Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, H. Comon, C. Kirchner, H. Kirchner
(réd.), 4600 , Springer. – jun 2007.
[67] G. Burel, C. Kirchner. – hh Completion is an Instance of Abstract Canonical
System Inference ii. – 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.
– San Diego, June 2006.
[68] G. Burel, C. Kirchner. – hh Cut Elimination in Deduction Modulo by Abstract Completion ii. – 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.
[69] C. Castro, C. Kirchner. – hh Constraint Rewriting ii. – In : Proceedings
of The Workshop on Applications of Rewriting, 9th International Conference
on Rewriting Techniques and Applications, RTA’98, Tsukuba, Japan. – March
1998.
[70] C. Castro, C. Kirchner. – hh Using Computational Systems as a General
Framework for Handling CSPs ii. – In : Proceedings of The Annual Workshop of The Constraints in Computational Logics Working Group, CCL’98 . –
Jerusalem, Israel, September 1998.
[71] H. Cirstea, C. Kirchner, L. Liquori. – hh Matching Power ii. – In : 12th International 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 Technical Report A01-R-201, LORIA, Nancy (France).
[72] H. Cirstea, C. Kirchner, L. Liquori. – hh The Rho Cube ii. – 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 Technical Report A01-R-202, LORIA, Nancy (France).
[73] H. Cirstea, C. Kirchner. – hh The rewriting calculus as a semantics of ELAN ii.
– 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.
6
[74] H. Cirstea, C. Kirchner. – hh Using Rewriting and Strategies for Describing
the B Predicate Prover ii. – In : Proceedings of the Workshop on Strategies in
Automated Deduction, CADE-15 . – Lindau, Germany, July 1998.
[75] H. Cirstea, C. Kirchner. – hh Combining Higher-Order and First-Order Computation Using Rho Calculus: Towards a Semantics of ELAN ii. – In : FroCoS’98, Amsterdam. – 1999.
[76] H. Cirstea, C. Kirchner. – hh The simply typed rewriting calculus ii. – In : 3rd
International Workshop on Rewriting Logic and its Applications - WRLA2000 .
– September 2000.
[77] A. S. de Oliveira, E. K. Wang, C. Kirchner, H. Kirchner. – hh Weaving
Rewrite-Based Access Control Policies ii. – In : Proceedings of 5th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code,
ACM Press. – George Mason University, USA, nov 2007.
[78] E. Deplagne, C. Kirchner, H. Kirchner, Q.-H. Nguyen. – hh Proof Search
and Proof Check for Equational and Inductive Theorems ii. – In : Proceedings
of CADE-19 , F. Baader (réd.), Lecture Notes in Computer Science, SpringerVerlag. – Miami, Florida, July 2003.
[79] E. Deplagne, C. Kirchner. – hh Deduction versus Computation: the Case
of Induction ii. – 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.
[80] N. Dershowitz, C. Kirchner. – hh Inversion Strategies ii. – In : Third Workshop on Rule-Based Constraint Reasoning and Programming (RCoRP’01). –
Paphos (Cyprus), December 2001.
[81] N. Dershowitz, C. Kirchner. – hh Abstract canonical inference systems ii. –
In : Proceedings of the UNIF’02 workshop. – July 2002.
[82] N. Dershowitz, C. Kirchner. – hh Abstract Saturation-Based Inference ii. –
In : Proceedings of LICS , P. Kolaitis (réd.), IEEE. – Ottawa, Ontario, June
2003.
[83] E. Domenjoud, C. Kirchner, J. Zhou. – hh Generating feasible schedules
for a pick-up and delivery problem ii. – In : Proceedings of the CP98 workshop on Large Scale Combinatorial Optimisation and Constraints, M. Wallace, Y. Caseau, E. Jacquet-Lagreze, H. Simonis, G. Pesant (réd.), Elsevier:
Electronic Notes in Discrete Mathematics, volume 1. – October 1998. texttthttp://www.elsevier.nl/locate/disc.
[84] D. J. Dougherty, C. Kirchner, H. Kirchner, A. S. de Oliveira. –
hh Modular Access Control Via Strategic Rewriting ii. –
In : Computer Security - ESORICS 2007, 12th European Symposium On Research In Computer
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.
7
[85] G. Dowek, T. Hardin, C. Kirchner, F. Pfenning. – hh Unification via Explicit Substitutions: The Case of Higher-Order Patterns ii. – In : Proceedings of
JICSLP’96 , M. Maher (réd.), The MIT press. – Bonn (Germany), September
1996.
[86] G. Dowek, T. Hardin, C. Kirchner. – hh Higher-order unification via explicit
substitutions, Extended abstract ii. – In : Proceedings of LICS’95 , D. Kozen
(réd.), pp. 366–374. – San Diego, June 1995.
[87] G. Dowek, T. Hardin, C. Kirchner. – hh HOL-λσ an intentional first-order
expression of higher-order logic ii. – In : RTA’99 . – June 1999.
[88] G. Dowek, T. Hardin, C. Kirchner. – hh HOL-λσ an intentional first-order
expression of higher-order logic ii. – In : Proceedings of RTA’99 , P. Narendran,
M. Rusinowitch (réd.), Lecture Notes in Computer Science, Springer-Verlag. –
June 1999.
[89] G. Dowek, T. Hardin, C. Kirchner. – hh A completeness theorem for an extension of first-order logic with binders ii. – In : Proceedings of the IJCAR workshop on Mechanized Reasoning about Languages with Variable Binding, R. Crole,
S. Ambler, A. Momigliano (réd.). – June 2001.
[90] G. Dowek, T. Hardin, C. Kirchner. – hh Binding Logic: proofs and models ii.
– In : Proceedings of the LPAR conference, M. Baaz, A. Voronkov (réd.), Lecture Notes in Computer Science, xx , Springer-Verlag, p. yy. – Tbilisi, Georgia,
October 2002.
[91] M. El Habib, C. Kirchner, H. Kirchner, J.-Y. Marion, S. Merz. – hh The
QSL platform at LORIA ii. – In : First QPQ Workshop on Deductive Software
Components, Miami, Floride. – Jun 2003.
[92] G. Faure, C. Kirchner. – hh Exceptions in the rewriting calculus ii. – In :
Proceedings of the RTA conference, S. Tison (réd.), Lecture Notes in Computer
Science, Springer-Verlag, pp. 66–82. – Copenhagen, July 2002.
[93] D. Fortin, C. Kirchner, P. Strogova. – hh Routing in Regular Networks
Using Rewriting ii. – In : Proceedings of the CADE international workshop on
automated reasoning in algebra (ARIA), J. Slaney (réd.), pp. 5–8. – June 1994.
[94] I. Gnaedig, C. Kirchner, H. Kirchner. – hh Equational Completion in Ordersorted Algebras ii. – 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.
[95] J. A. Goguen, C. Kirchner, H. Kirchner, A. Mégrelis, J. Meseguer,
T. Winkler. – hh An Introduction to OBJ-3 ii. – In : Proceedings 1st International 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.
[96] J. A. Goguen, C. Kirchner, J. Meseguer, T. Winkler. – hh OBJ as a Language for Concurrent Programming ii. – In : Proceedings of Second International
8
Supercomputing Conference, Volume I , S. Kartashev, S. Kartashev (réd.), International Supercomputing Institute, Inc., pp. 195–198. – Santa Clara (CA,
USA), 1987.
[97] J. A. Goguen, C. Kirchner, J. Meseguer. – hh Concurrent Term Rewriting
as a Model of Computation ii. – In : Proceedings of Graph Reduction Workshop,
R. Keller, J. Fasel (réd.), Lecture Notes in Computer Science, 279 , SpringerVerlag, pp. 53–93. – Santa Fe (NM, USA), 1987.
[98] C. Hintermeier, C. Kirchner, H. Kirchner. – hh Strict Matchings and Unifications in G-algebras ii. – In : Proceedings of the 9th WADT - 4th Compass
Workshop. – 1992. Centre de Recherche en Informatique de Nancy, 92-R-268.
[99] C. Hintermeier, C. Kirchner, H. Kirchner. – hh Dynamically-Typed Computations for Order-Sorted Equational Presentations –Extended Abstract– ii. –
In : Proc. 21st International Colloquium on Automata, Languages, and Programming, S. Abiteboul, E. Shamir (réd.), Lecture Notes in Computer Science,
820 , Springer-Verlag, pp. 450–461. – 1994.
[100] C. Hintermeier, C. Kirchner, H. Kirchner. – hh Order-Sorted Completion
with Dynamic Types ii. – In : Proceedings of the 10th WADT – 6th Compass
Workshop. – May 1994.
[101] C. Hintermeier, C. Kirchner, H. Kirchner. – hh Sort Inheritance for OrderSorted Equational Presentations ii. – In : Recent Trends in Data Types Specification, Lecture Notes in Computer Science, 906 , Springer-Verlag, pp. 319–335.
– 1995.
[102] J.-P. Jouannaud, C. Kirchner, H. Kirchner, A. Mégrelis. – hh OBJ: Programming with equalities, subsorts, overloading and parameterization ii. – In :
Proceedings 1st International Workshop on Algebraic and Logic Programming,
49 , Akademie-Verlag, pp. 41–52. – November 1988. Report CRIN 88-R-148.
[103] J.-P. Jouannaud, C. Kirchner, H. Kirchner, M. Picard. – hh Les arbres
signés : un cadre algébrique pour la résolution d’équation dans les arbres ii. –
In : Proceedings of Congrès AFCET-Informatique Nancy. – 1980.
[104] J.-P. Jouannaud, C. Kirchner, H. Kirchner. – hh Incremental unification in
equational theories ii. – In : Proceedings of the Allerton conference. – Allerton
(USA), 1982.
[105] J.-P. Jouannaud, C. Kirchner, H. Kirchner. – hh Incremental Construction of Unification Algorithms in Equational Theories ii. – In : Proceedings International Colloquium on Automata, Languages and Programming, Barcelona
(Spain), J. Dı́az (réd.), Lecture Notes in Computer Science, 154 , SpringerVerlag, pp. 361–373. – 1983.
[106] C. Kirchner, H. Kirchner, J.-P. Jouannaud. – hh Algebraic manipulations
as a unification and matching strategy for linear equations in signed binary
trees ii. – In : Proceedings of IJCAI’81 . – Vancouver (Canada), 1981.
9
[107] C. Kirchner, H. Kirchner, J. Meseguer. – hh Operational semantics of OBJ3 ii. – In : Proceedings of 15th International Colloquium on Automata, Languages
and Programming, Lecture Notes in Computer Science, 317 , Springer-Verlag,
pp. 287–301. – 1988.
[108] C. Kirchner, H. Kirchner, M. Vittek. – hh Designing Constraint Logic Programming Languages using Computational Systems ii. – In : Proceedings of the
2nd CCL Workshop, La Escala (Spain), F. Orejas (réd.). – September 1993.
[109] C. Kirchner, H. Kirchner, M. Vittek. – hh Implementing Computational
Systems with Constraints ii. – In : Proceedings of the first Workshop on Principles and Practice of Constraint Programming, Providence (R.I., USA), P. Kanellakis, J.-L. Lassez, V. Saraswat (réd.), Brown University, pp. 166–175. – 1993.
[110] C. Kirchner, H. Kirchner. – hh Trois méthodes de résolution d’équations
dans les algèbres libres et les variétés équationnelles d’algèbres ii. – In : Actes
des journées GROPLAN-GRECO Programmation, Bergerac. – 1982.
[111] C. Kirchner, H. Kirchner. – hh Nouvelles applications du système REVE ii. –
In : Actes du Séminaire LITP . – 1984.
[112] C. Kirchner, H. Kirchner. – hh Implementation of a general completion procedure parametrized by built-in theories and strategies ii. – In : Proceedings of
the EUROCAL Conference, Linz (Austria), B. Buchberger (réd.), Lecture Notes
in Computer Science, 204 , Springer-Verlag. – 1985.
[113] C. Kirchner, H. Kirchner. – hh Constrained Equational Reasoning ii. – 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.
[114] C. Kirchner, H. Kirchner. – hh Rule-Based Programming and Proving: The
ELAN Experience Outcomes ii. – 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.
[115] C. Kirchner, F. Klay. – hh A Note on Syntacticness ii. – In : Proceedings 3rd
International Workshop on Unification, Lambrecht (Germany), H.-J. Bürckert,
W. Nutt (réd.). – June 1989.
[116] C. Kirchner, F. Klay. – hh Syntactic Theories and Unification ii. – In : Proceedings 5th IEEE Symposium on Logic in Computer Science, Philadelphia (Pa.,
USA), pp. 270–277. – June 1990.
[117] C. Kirchner, R. Kopetz, P.-E. Moreau. – hh Anti-Pattern Matching ii. – In :
16th European Symposium on Programming (ESOP’07). – Braga, Portugal,
2007.
[118] C. Kirchner, P. Lescanne. – hh Solving Disequations ii. – 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] C. Kirchner, C. Lynch, C. Scharff. – hh A Fine-grained Concurrent Completion Procedure ii. – In : Proceedings of RTA’96 , H. Ganzinger (réd.), Lecture
Notes in Computer Science, 1103 , Springer-Verlag, pp. 3–17. – September 1996.
[120] C. Kirchner, P.-E. Moreau, A. Reilles. – hh Formal validation of pattern
matching code. ii. – In : Barahona et Felty [2], pp. 187–197.
[121] C. Kirchner, C. Ringeissen. – hh Higher-order equational unification via explicit substitutions ii. – In : Proceedings of the tenth UNIF Workshop, K. U.
Schulz, S. Kepser (réd.). – Munich, Germany, June 1996.
[122] C. Kirchner, C. Ringeissen. – hh Higher-Order Equational Unification via
Explicit Substitutions ii. – In : Proceedings 6th International Joint Conference ALP/HOA’97 , Lecture Notes in Computer Science, 1298 , Springer-Verlag,
pp. 61–75. – Southampton (UK), September 1997.
[123] C. Kirchner, P. Viry. – hh Implementing Parallel Rewriting ii. – In : Parallelization in Inference Systems, B. Fronhöfer, G. Wrightson (réd.), Lecture Notes
in Artificial Intelligence, 590 , Springer-Verlag, pp. 123–138. – 1992.
[124] C. Kirchner. – hh A New Equational Unification Method: A Generalization of
Martelli-Montanari Algorithm ii. – 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.
[125] C. Kirchner. – hh Computing unification algorithms ii. – In : Proceedings 1st
IEEE Symposium on Logic in Computer Science, Cambridge (Mass., USA),
pp. 206–216. – 1986.
[126] C. Kirchner. – hh ELAN : Modélisation et preuve en calcul de réécriture
(présentation invitée) ii. – 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).
[127] C. Kirchner. – hh Strategic Rewriting ii. – In : 4th International Workshop
on Reduction Strategies in Rewriting and Programming - WRS’2004, Aachen,
Germany. – Jun 2004.
[128] P. Réty, C. Kirchner, H. Kirchner, P. Lescanne. – hh Narrower: A new
algorithm for unification and its application to logic programming ii. – 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.
[129] Horatiu Cirstea, Claude Kirchner, Luigi Liquori, Benjamin Wack. –
hh Rewrite Strategies in the Rewriting Calculus ii. – 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.
[130] Horatiu Cirstea, Claude Kirchner, Luigi Liquori. – hh Rewriting Calculus
with(out) Types ii. – In : Proceedings of the fourth workshop on rewriting logic
and applications, F. Gadducci, U. Montanari (réd.), 71 , Electronic Notes in
Theoretical Computer Science, pp. 3–19. – Pisa (Italy), 2002.
11
Internal publications and technical reports
[131] P. Borovanský, 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.
[132] 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.
[133] C. Castro, C. Kirchner. – hh Towards a Methodology for Rule-Based Programming ii. – technical report, LORIA, December 2002.
[134] H. Cirstea, C. Kirchner. – hh An introduction to the rewriting calculus ii. –
Research Report RR-3818 , INRIA, December 1999.
[135] E. Domenjoud, C. Kirchner, J. Zhou. – Le manuel de ROUTER. – LORIA,
October 1998.
[136] E. Domenjoud, C. Kirchner, J. Zhou. – hh The ROUTER transport scheduling
system ii. – Technical report, LORIA, October 1998.
[137] G. Dowek, T. Hardin, C. Kirchner. – hh Higher-order unification via explicit substitutions ii. – Rapport RR-2709 , INRIA Lorraine, November 1995. –
available under: http://www.loria.fr/equipe/protheo.html.
[138] G. Dowek, T. Hardin, C. Kirchner. – hh HOL-λσ an intentional first-order
expression of higher-order logic ii. – Rapport de Recherche 3556 , Institut National de Recherche en Informatique et en Automatique, November 1998.
[139] G. Dowek, T. Hardin, C. Kirchner. – hh Theorem Proving Modulo ii. – Rapport de Recherche 3400 , Institut National de Recherche en Informatique et en
Automatique, April 1998. – .
[140] G. Dowek, T. Hardin, C. Kirchner. – hh Theorem Proving Modulo, revised
version ii. – Rapport de Recherche 4861 , Institut National de Recherche en
Informatique et en Automatique, July 2003.
[141] I. Gnaedig, C. Kirchner, H. Kirchner. – hh Equational Completion in Ordersorted Algebras ii. – Rapport 87-R-086 , Centre de Recherche en Informatique
de Nancy, 1987.
[142] J. A. Goguen, C. Kirchner, J. Meseguer. – hh Models of computation for
the rewrite rule machine ii. – Technical report 86-R-104 , Centre de Recherche
en Informatique de Nancy, 1986.
[143] C. Kirchner, H. Kirchner, A. Mégrelis. – hh OBJ for OBJ ii. – Rapport
87-R-085 , Centre de Recherche en Informatique de Nancy, 1987.
[144] C. Kirchner, H. Kirchner, F. Nahon. –
Search ii. – Rapport, LORIA, 2006.
hh
Narrowing Based Inductive Proof
[145] C. Kirchner, H. Kirchner, M. Rusinowitch. –
constraints ii. – Rapport 1358 , INRIA, 1990.
12
hh
Deduction with symbolic
[146] C. Kirchner, H. Kirchner, M. Vittek. – ELAN V 1.17 User Manual . –
Inria Lorraine & Crin, Nancy (France), November 1995.
[147] C. Kirchner, H. Kirchner. – hh Solving equations in the signed trees theory.
Application to program derecursivation ii. – Rapport interne 81-R-056 , Centre
de Recherche en Informatique de Nancy, 1981.
[148] C. Kirchner, H. Kirchner. – hh Manuel d’utilisation de Aidarbre, un éditeur
d’arbres ii. – Rapport interne 82-R-042 , Centre de Recherche en Informatique
de Nancy, 1982.
[149] C. Kirchner, H. Kirchner. – hh Unification dans les théories équationnelles ii.
– Rapport interne 83-R-011 , Centre de Recherche en Informatique de Nancy,
1983.
[150] C. Kirchner, H. Kirchner. – hh Constrained Equational Reasoning for Completion ii. – Research report 89-R-222 , Centre de Recherche en Informatique de
Nancy, 1989. – Proceedings of UNIF’89, 1989.
[151] C. Kirchner, H. Kirchner. – hh Rewriting: theory and applications ii. – Research report 89-E-225 , Centre de Recherche en Informatique de Nancy, 1989.
– DEA lecture.
[152] C. Kirchner, Z. Qian, P.-K. Singh, J. Stuber. –
of XSLT in ELAN ii. – Rapport, LORIA, 2001.
hh
Xemantics: A semantics
[153] C. Kirchner. – hh Etude comparative des formateurs MINT, GROFF, NROFF
associes aux editeurs Emacs, VI, Emin : Rapport de fin de contrat ii. – Rapport
interne 85-R-091 , Centre de Recherche en Informatique de Nancy, 1985.
[154] F. Klay, E. Domenjoud, C. Kirchner. – hh Vérification Sémantique de
Spécifications Métallurgiques ii. – Rapport de fin de contrat, Inria Lorraine &
Crin, 1993.
[155] P. Réty, C. Kirchner, H. Kirchner, P. Lescanne. – hh An algorithm for unification based on narrowing ii. – Rapport CRIN 86-R-131 , Centre de Recherche
en Informatique de Nancy, 1986.
Miscellaneous
[156] F. Ajili, C. Castro, E. Domenjoud, C. Kirchner. – hh Rapport de fin de
pré-étude du problème d’affectation des courses pour le GIHP-Champagne ii. –
Rapport de fin de contrat, November 1996.
[157] C. Kirchner, H. Kirchner. – hh Rewriting, Solving, Proving ii. – A preliminary
version of a book available at , 1999.
[158] C. Kirchner. – hh Order-sorted Equational Unification ii. – Presented at the
fifth International Conference on Logic Programming (Seattle, USA), August
1988. – Also as rapport de recherche INRIA 954, Dec. 88.
[159] C. Kirchner. –
hh
Unifications ii. – Cours de DEA, 1989.
13
[160]
hh
UNIF’87. Extended Abstracts of the First International Workshop on Unification ii, 1987. – CRIN report 87-R-34.
[161]
hh
UNIF’88. Extended Abstracts of the 2nd International Workshop on Unification ii, 1988. – CRIN report 89-R-38.
14