Software Engineering

[33] Pietro Abate and Roberto Di Cosmo. Adoption of academic tools in open source communities: the Debian case study. In OSS 2017, pages 139--150. Springer, 2017.
[32] Federico Balaguer, Roberto Di Cosmo, Alejandra Garrido, Fabio Kon, Gregorio Robles, and Stefano Zacchiroli, editors. Open Source Systems: Towards Robust Practices - 13th IFIP WG 2.13 International Conference, OSS 2017, Buenos Aires, Argentina, May 22-23, 2017, Proceedings, volume 496 of IFIP Advances in Information and Communication Technology, 2017.
[31] Pietro Abate, Roberto Di Cosmo, Louis Gesbert, Fabrice Le Fessant, Ralf Treinen, and Stefano Zacchiroli. Mining component repositories for installability issues. In Massimiliano Di Penta, Martin Pinzger, and Romain Robbes, editors, 12th IEEE/ACM Working Conference on Mining Software Repositories, MSR 2015, Florence, Italy, May 16-17, 2015, pages 24--33. IEEE, 2015.
[30] Maëlick Claes, Tom Mens, Roberto Di Cosmo, and Jérôme Vouillon. A historical analysis of debian package incompatibilities. In Massimiliano Di Penta, Martin Pinzger, and Romain Robbes, editors, 12th IEEE/ACM Working Conference on Mining Software Repositories, MSR 2015, Florence, Italy, May 16-17, 2015, pages 212--223. IEEE, 2015.
[29] Roberto Di Cosmo, Michael Lienhardt, Jacopo Mauro, Stefano Zacchiroli, Gianluigi Zavattaro, and Jakub Zwolakowski. Automatic application deployment in the cloud: from practice to theory and back (invited paper). In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 1--16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
[28] Pietro Abate, Roberto Di Cosmo, Ralf Treinen, and Stefano Zacchiroli. Learning from the future of component repositories. Science of Computer Programming, 90(B):93--115, September 2014.
[27] Jérôme Vouillon, Mehdi Dogguy, and Roberto Di Cosmo. Easing software component repository evolution. In Pankaj Jalote, Lionel C. Briand, and André van der Hoek, editors, 36th International Conference on Software Engineering, ICSE '14, Hyderabad, India - May 31 - June 07, 2014, pages 756--766. ACM, 2014.
[26] Roberto Di Cosmo, Michael Lienhardt, Ralf Treinen, Stefano Zacchiroli, Jakub Zwolakowski, Antoine Eiche, and Alexis Agahi. Automated synthesis and deployment of cloud applications. In Ivica Crnkovic, Marsha Chechik, and Paul Grünbacher, editors, ACM/IEEE International Conference on Automated Software Engineering, ASE '14, Vasteras, Sweden - September 15 - 19, 2014, pages 211--222. ACM, 2014.
[25] Roberto Di Cosmo, Jacopo Mauro, Stefano Zacchiroli, and Gianluigi Zavattaro. Aeolus: A component model for the cloud. Information and Computation, 239:100--121, 2014.
[24] Pietro Abate, Roberto Di Cosmo, Ralf Treinen, and Stefano Zacchiroli. A modular package manager architecture. Information and Software Technology, 55(2):459 -- 474, 2013. Special Section: Component-Based Software Engineering (CBSE), 2011.
[23] Jérôme Vouillon and Roberto Di Cosmo. Broken sets in software repository evolution. In ICSE, pages 412--421, 2013.
[22] Roberto Di Cosmo, Jacopo Mauro, Stefano Zacchiroli, and Gianluigi Zavattaro. Component reconfiguration in the presence of conflicts. In ICALP (2), pages 187--198, 2013.
[21] Michel Catan, Roberto Di Cosmo, Antoine Eiche, Tudor A. Lascu, Michael Lienhardt, Jacopo Mauro, Ralf Treinen, Stefano Zacchiroli, Gianluigi Zavattaro, and Jakub Zwolakowski. Aeolus: Mastering the complexity of cloud application deployment. In ESOCC, pages 1--3, 2013.
[20] Jérôme Vouillon and Roberto Di Cosmo. On software component co-installability. ACM Trans. Softw. Eng. Methodol., 22(4):34, 2013.
[19] Pietro Abate, Roberto Di Cosmo, Ralf Treinen, and Stefano Zacchiroli. Dependency solving: a separate concern in component evolution management. Journal of System and Software Science, 85(10):2228 -- 2240, 2012. Automated Software Evolution.
[18] Roberto Di Cosmo, Stefano Zacchiroli, and Gianluigi Zavattaro. Towards a formal component model for the cloud. In SEFM, pages 156--171, 2012.
[17] Roberto Di Cosmo, Ralf Treinen, and Stefano Zacchiroli. Formal aspects of free and open source software components - a short survey. In FMCO, pages 216--239, 2012.
[16] Pietro Abate, Roberto Di Cosmo, Ralf Treinen, and Stefano Zacchiroli. Learning from the future of component repositories. In Proceedings of the 15th ACM SIGSOFT symposium on Component Based Software Engineering, CBSE '12, pages 51--60, New York, NY, USA, 2012. ACM.
[15] Roberto Di Cosmo, Davide Di Ruscio, Patrizio Pelliccione, Alfonso Pierantonio, and Stefano Zacchiroli. Supporting software evolution in component-based FOSS systems. Science of Computer Programming, 76(12):1144--1160, December 2011.
[14] Pietro Abate and Roberto Di Cosmo. Predicting upgrade failures using dependency analysis. In Serge Abiteboul, Klemens Böhm, Christoph Koch, and Kian-Lee Tan, editors, Workshops Proceedings of the 27th International Conference on Data Engineering, ICDE 2011, April 11-16, 2011, Hannover, Germany, pages 145--150. IEEE, 2011.
[13] Pietro Abate, Roberto Di Cosmo, Ralf Treinen, and Stefano Zacchiroli. Mpm: a modular package manager. In Proceedings of the 14th international ACM Sigsoft symposium on Component based software engineering, CBSE '11, pages 179--188, New York, NY, USA, 2011. ACM.
[12] Roberto Di Cosmo and Jérôme Vouillon. On software component co-installability. In Tibor Gyimóthy and Andreas Zeller, editors, SIGSOFT/FSE'11 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-19) and ESEC'11: 13rd European Software Engineering Conference (ESEC-13), Szeged, Hungary, September 5-9, 2011, pages 256--266. ACM, 2011.
[11] Roberto Di Cosmo, Olivier Lhomme, and Claude Michel. Aligning component upgrades. In Conrad Drescher, Inês Lynce, and Ralf Treinen, editors, Proceedings Second Workshop on Logics for Component Configuration, volume 65, pages 1--11, 2011.
[10] Roberto Di Cosmo and Jaap Boender. Using strong conflicts to detect quality issues in component-based complex systems. In ISEC '10: Proceedings of the 3rd India software engineering conference, pages 163--172, New York, NY, USA, 2010. ACM.
[9] Roberto Di Cosmo and Stefano Zacchiroli. Feature diagrams as package dependencies. In Jan Bosch and Jaejoon Lee, editors, Software Product Lines: Going Beyond - 14th International Conference, SPLC 2010, Jeju Island, South Korea. Proceedings, volume 6287 of Lecture Notes in Computer Science, pages 476--480. Springer, 13-17 September 2010.
[8] Pietro Abate, Jaap Boender, Roberto Di Cosmo, and Stefano Zacchiroli. Strong dependencies between software components. In International Symposium on Empirical Sofware Engineering and Measurement, pages 89--99. IEEE Press, October 2009.
[7] Jaap Boender, Roberto Di Cosmo, Jérôme Vouillon, Berke Durak, and Fabio Mancinelli. Improving the quality of gnu/linux distributions. In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference, COMPSAC 2008, 28 July - 1 August 2008, Turku, Finland, pages 1240--1246. IEEE Computer Society, 2008.
[6] Roberto Di Cosmo, Stefano Zacchiroli, and Paulo Trezentos. Package upgrades in FOSS distributions: details and challenges. In HotSWUp '08: Proceedings of the 1st International Workshop on Hot Topics in Software Upgrades, pages 1--5, New York, NY, USA, 2008. ACM.
[5] Jaap Boender, Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, Mario Morgado, David Pinheiro, Ralf Treinen, Paulo Trezentos, and Jérôme Vouillon. News from the EDOS project: improving the maintenance of free software distributions. In Olivier Berger, editor, Proceedings of the 7th International Workshop on Free Software (IWFS'06), pages 199 -- 207, Porto Alegre, Brazil, April 2006.
[4] Roberto Di Cosmo, Fabio Mancinelli, Jaap Boender, Jerome Vouillon, Berke Durak, Xavier Leroy, David Pinheiro, Paulo Trezentos, Mario Morgado, Tova Milo, Tal Zur, Rafael Suarez, Marc Lijour, and Ralf Treinen. Report on formal mangement of software dependencies. Technical report, EDOS, April 2006. EDOS project Deliverable 2.2, available as http://hal-univ-diderot.archives-ouvertes.fr/docs/00/69/74/68/PDF/edos-wp2d2.pdf.
[3] Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, and Jérôme Vouillon. Maintaining large software distributions: new challenges from the FOSS era. In Proceedings of the FRCSS 2006 workshop, 2006. EASST Newsletter.
[2] Fabio Mancinelli, Jaap Boender, Roberto Di Cosmo, Jerome Vouillon, Berke Durak, Xavier Leroy, and Ralf Treinen. Managing the complexity of large free and open source package-based software distributions. In Sebastian Uchitel and Steve Easterbrook, editors, 21st IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 199--208. IEEE Computer Society, 2006.
[1] Serge Abiteboul, Ciarán Bryce, Roberto Di Cosmo, Klaus R. Dittrich, Stéfane Fermigier, Stéphane Laurière, Frédéric Lepied, Xavier Leroy, Tova Milo, Eleonora Panto, Radu Pop, Assaf Sagi, Yotam Shtossel, Florent Villard, and Boris Vrdoljak. EDOS: Environment for the Development and Distribution of Open Source Software. In First International Conference on Open Source Systems (OSS 2005), 2005.

Parallel Programming

[13] Marco Danelutto and Roberto Di Cosmo. A "Minimal Disruption" skeleton experiment: Seamless map & reduce embedding in OCaml. Procedia CS, 9:1837--1846, 2012.
[12] Roberto Di Cosmo, Zheng Li, Susanna Pelagatti, and Pierre Weis. Skeletal parallel programming with ocamlp3l 2.0. Parallel Processing Letters, 18(1):149--164, March 2008.
[11] Roberto Di Cosmo, Zheng Li, and Susanna Pelagatti. A calculus for parallel computations over multidimensional dense arrays. Computer Languages, Systems and Structures, 33(3-4):82--110, 2007.
[10] François Clément, Vincent Martin, Arnaud Vodicka, Roberto Di Cosmo, and Pierre Weis. Domain decomposition and skeleton programming with OCamlP3l. Parallel Computing, 32:539--550, 2006. Special Issue on Algorithmic Skeletons, extended version of  [9].
[9] François Clément, Vincent Martin, Arnaud Vodicka, Roberto Di Cosmo, and Pierre Weis. Domain decomposition and skeleton programming with OCamlP3l. In G. R. Joubert, W. E. Nagel, F. J. Peters, O. Plata, P. Tirado, and E. Zapata, editors, Proc. of the Internat. Conf. on Parallel Computing: Current & Future Issues of High-End Computing, volume 33 of J. von Neumann Institute for Computing (NIC), pages 811--818. NIC-Directors, 2006.
[8] Roberto Di Cosmo, Zheng Li, Susanna Pelagatti, and Pierre Weis. Skeletal parallel programming with ocamlp3l 2.0. Third International Workshop on High-level Parallel Programming and Applications, 4-5July 2005.
[7] F. Clément, V. Martin, A. Vodicka, R. Di Cosmo, and P. Weis. Domain decomposition for flow simulation around a waste disposal site: direct computation versus code coupling using ocamlp3l. International Conference on Supercomputing in Nuclear Applications (SNA'2003), September 2003.
[6] F. Clément, A. Li, V. Martin, A. Vodicka, R. Di Cosmo, and P. Weis. Parallel programming with the ocamlp3l system, with applications to coupling numerical codes. Journal of Functional Programming, September 2003. Submitted.
[5] Roberto Di Cosmo and Susanna Pelagatti. A calculus for dense array distributions. Second International Workshop on High-Level Parallel Programming and Applications, 2003.
[4] François Clément, Arnaud Vodicka, Roberto Di Cosmo, and Pierre Weis. Couplage de codes numériques, parallélisme et langages de haut niveau. RR 4825, INRIA, 2003. http://www.inria.fr/rrrt/rr-4825.html.
[3] Roberto Di Cosmo and Susanna Pelagatti. A calculus for dense array distributions. Parallel Processing Letters, 13(3):377--388, 2003.
[2] Marco Danelutto, Roberto Di Cosmo, Xavier Leroy, and Susanna Pelagatti. OcamlP3l: a functional parallel programming system. Technical Report 98-01, LIENS - DMI, Ecole Normale Supérieure, 1998.
[1] Marco Danelutto, Roberto Di Cosmo, Xavier Leroy, and Susanna Pelagatti. Parallel functional programming with skeletons: the OCamlP3L experiment. In Proceedings ACM workshop on ML and its applications, Baltimore, 1998. Cornell University.

Type Isomorphisms

[20] Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta. On isomorphisms of intersection types. ACM Transactions on Computational Logic, 11(4):1--24, 2010.
[19] Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta. On isomorphisms of intersection types. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 461--477. Springer, 2008.
[18] Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. Annals of Pure and Applied Logic, 141(1--2):35--50, August 2006.
[17] Roberto Di Cosmo and Sergei Soloviev, editors. Special Issue on Type Isomorphisms. Cambridge University Press, 2005. Vol. 15.
[16] Roberto Di Cosmo. A short survey of isomorphisms of types. Mathematical Structures in Computer Science, 15:825--838, 2005.
[15] Roberto Di Cosmo, François Pottier, and Didier Rémy. Subtyping recursive types modulo associative commutative products. Typed Lambda Calculus and Applications, 2005.
[14] Vincent Balat, Roberto Di Cosmo, and Marcelo Fiore. Remarks on isomorphisms in typed lambda calculi with empty and sum type. In LICS. IEEE, July 2002.
[13] Roberto Di Cosmo. Réécriture avec axiomes extensionnels et isomorphismes de types. Habilitation à diriger des recherches, Université de Paris VII, 2, place Jussieu - 75005 Paris, April 1998.
[12] D. Delahaye, Roberto Di Cosmo, and B. Werner. Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes. In PRC/GDR de programmation, Pôle Preuves et Spécifications Algébriques, November 1997.
[11] Maria-Virginia Aponte, Roberto Di Cosmo, and Catherine Dubois. Signature subtyping modulo type isomorphisms. submitted, 1997.
[10] Maria-Virginia Aponte and Roberto Di Cosmo. Type isomorphisms for module signatures. In Programming Languages Implementation and Logic Programming (PLILP), volume 1140 of Lecture Notes in Computer Science, pages 334--346. Springer-Verlag, 1996.
[9] Roberto Di Cosmo. Second order isomorphic types. A proof theoretic study on second order λ-calculus with surjective pairing and terminal object. Information and Computation, pages 176--201, June 1995.
[8] Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhauser, 1995. ISBN-0-8176-3763-X.
[7] Roberto Di Cosmo. Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, 3(3):485--525, 1993. Special Issue on ML.
[6] Roberto Di Cosmo. Isomorphisms of Types. Tesi di dottorato, Dipartimento di Informatica, Universitá di Pisa, 40, Corso Italia - 56100 Pisa - Italy, January 1993.
[5] Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231--247, 1992.
[4] Roberto Di Cosmo. Type isomorphisms in a type assignment framework. In 19th Ann. ACM Symp. on Principles of Programming Languages (POPL), pages 200--210. ACM, 1992.
[3] Roberto Di Cosmo and Giuseppe Longo. Constuctively equivalent propositions and isomorphisms of objects (or terms as natural transformations). In Moschovakis, editor, Logic from Computer Science, volume 21 of Mathematical Sciences Research Institute Publications, pages 73--94. Springer Verlag, Berkeley, 1991.
[2] Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Technical Report 90-14, LIENS - Ecole Normale Supérieure, 1990.
[1] Roberto Di Cosmo. Isomorfismi di tipi. Master's thesis, Università di Pisa, 1986.

Linear Logic

[7] Roberto Di Cosmo, Delia Kesner, and Emmanuel Polonovski. Proof nets and explicit substitutions. Mathematical Structures in Computer Science, 13(3):409--450, June 2003.
[6] Roberto Di Cosmo, Delia Kesner, and Emmanuel Polonovski. Proof nets and explicit substitutions. In Foundation of Software Science and Computation Structure, volume 1784 of Lecture Notes in Computer Science, pages 63--81. Springer-Verlag, 2000.
[5] Vincent Balat and Roberto Di Cosmo. A linear logical view of linear type isomorphisms. In Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 250--265. Springer-Verlag, 1999.
[4] Roberto Di Cosmo and Delia Kesner. Strong normalization of explicit substitutions via cut elimination in proof nets (extended abstract). In Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 35--46, Warsaw, Poland, 29 June- 2July 1997. IEEE Computer Society Press.
[3] Vincent Danos and Roberto Di Cosmo. The Linear Logic Primer. 1997. In preparation: preliminary version available from http://www.dicosmo.org.
[2] Vincent Danos and Roberto Di Cosmo. Introduction to linear logic. Course Notes, very preliminary version of [3], June 1992.
[1] Roberto Di Cosmo and Dale Miller. Linear logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Fall 2006.

Rewriting

[17] Vincent Balat, Roberto Di Cosmo, and Marcelo Fiore. Extensional normalisation and type-directed partial evaluation for typed lamda calculus with sums. In 31st Ann. ACM Symp. on Principles of Programming Languages (POPL), pages 64--76. ACM, 2004.
[16] Roberto Di Cosmo and Stefano Guerrini. Strong normalization of proof nets modulo structural congruences. In Rewriting Techniques and Applications, 1999.
[15] Roberto Di Cosmo and Neil Ghani. Combining algebraic rewriting with higher order extensional lambda calculi. In Pierpaolo Degano, Roberto Gorrieri, and Alberto Marchetti-Spaccamela, editors, Intern. Conf. on Automata, Languages and Programming (ICALP)24, number 1256 in Lecture Notes in Computer Science, pages 237--247, 1997.
[14] Roberto Di Cosmo. A brief history of rewriting with extensionality. In Fairouz Kamareddine, editor, International Summer School on Type Theory and Rewriting, Glasgow, September 1996. Kluwer. A set of slides on the subject is available as http://www.dicosmo.org/Slides/GLA96.ps.gz.
[13] Roberto Di Cosmo. On the power of simple diagrams. In Rewriting Techniques and Applications, number 1103 in Lecture Notes in Computer Science, pages 200--214, July 1996.
[12] Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λ-calculus with surjective pairing and terminal object. Journal of Functional Programming, 6(2):299--327, 1996. This is an extended and revised version of [3].
[11] Roberto Di Cosmo and Delia Kesner. Combining algebraic rewriting, extensional lambda calculi and fixpoints. Theoretical Computer Science, 169(2):201--220, 1996.
[10] Roberto Di Cosmo and Delia Kesner. Rewriting with polymorphic extensional λ-calculus. In CSL'95, volume 1092 of Lecture Notes in Computer Science, pages 215--232. Springer-Verlag, 1996. Extended abstract presented in Paderborn, September 1995.
[9] Roberto Di Cosmo. An extensional operational and axiomatic semantics for type-inference with recursion and algebraic data types. October 1995.
[8] Roberto Di Cosmo and Adolfo Piperno. Expanding extensional polymorphism. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, pages 139--153, April 1995.
[7] Roberto Di Cosmo and Delia Kesner. Combining first order algebraic rewriting systems, recursion and extensional lambda calculi. In Serge Abiteboul and Eli Shamir, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 820 of Lecture Notes in Computer Science, pages 462--472. Springer-Verlag, July 1994.
[6] Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 4:1--48, 1994.
[5] Roberto Di Cosmo and Delia Kesner. A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object. In Andrzej Lingas, editor, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 700 of Lecture Notes in Computer Science, pages 645--656. Springer-Verlag, July 1993.
[4] Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Technical Report LIENS-93-11/INRIA 1911, LIENS-DMI and INRIA, 1993.
[3] Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λ-calculus with surjective pairing and terminal object. In Leach, Monien, and Artalejo, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 510 of Lecture Notes in Computer Science, pages 291--302. Springer-Verlag, July 1991.
[2] Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λ-calculus with surjective pairing and terminal object. Technical Report 91-11, LIENS - Ecole Normale Supérieure, 1991.
[1] Roberto Di Cosmo. Invertibility of terms and valid isomorphisms. a proof theoretic study on second order λ-calculus with surjective pairing and terminal object. Technical Report 91-10, LIENS - Ecole Normale Supérieure, 1991.

Number Theory

[1] Roberto Di Cosmo and Thomas Dufour. The equational theory of <n,0,1,+,·,> is decidable, but not finitely axiomatisable. In LPAR'05, Lecture Notes in Computer Science, pages 240--256, 2005.

Privacy and Security

[1] Roberto Di Cosmo. On privacy and anonymity in electronic and non electronic voting: the ballot-as-signature attack. April 2007.

Logic Programming

[3] Roberto Di Cosmo and Jean-Vincent Loddo. Playing logic programs with the alpha-beta algorithm. In Michel Parigot and Adrei Voronkov, editors, LPAR'00, volume 1955 of Lecture Notes in Computer Science, pages 207--224, 2000.
[2] Roberto Di Cosmo, Jean-Vincent Loddo, and Stéphane Nicolet. A game semantics foundation for logic programming. In Catuscia Palamidessi, Hugh Glaser, and Karl Meinke, editors, PLILP'98, volume 1490 of Lecture Notes in Computer Science, pages 355--373, 1998.
[1] Hassan Aït-Kaci and Roberto Di Cosmo. Compiling order-sorted feature term unification. TN 7, Digital Equipment Corporation, December 1993.