Jean-Jacques Lévy's Publications [back]

• Mechanizable proofs about parallel processes, with Jean-Marie Cadiou, 14th Annual IEEE Symposium on Switching and Automata Theory (SWAT 1973), 1973.

• Réductions sures dans le lambda-calcul, Paris 7, thèse de 3ème cycle, June, 1974. [Pdf, 4.7MB] (In French)

• An algebraic interpretation of the lambda-beta-K-calculus; and an application of a labelled lambda-calculus, Proceedings of the Rome Symposium on the Lambda calculus, 1975; also in Theoretical Computer Science 2 (1976), North Holland, pp.97-114. [Pdf]

• A structure oriented program editor: a first step towards computer assisted programming, with Véronique Donzeau-Gouge, Gérard Huet, Gilles Kahn, Bernard Lang, JJL, International Computing Symposium, North Holland, 1975

• Minimal and Optimal Computations of Recursive Programs, with Gérard Berry, Journal of the ACM, Vol 26, 1, Jan 1979, pp.148-175. [Pdf]. Also presented at the Fourth Annual ACM Symposium on Principles of Programming Languages (POPL) 1977.

• Réductions correctes et optimales dans le lambda-calcul, Paris 7, thèse d'Etat, January, 1978. [Pdf, 11.3MB] (In French)

• Le problème du partage dans l'évaluation des lambda-expressions, 1er colloque AFCET-SMF de Mathématiques Appliquées, Palaiseau, 4-8 Sept 1978. (In French)

• Approximations et Arbres de Bohm dans le lambda-calcul, Lambda Calcul et Sémantique formelle des langages de programmation, Actes de la 6ème école de printemps d'Informatique théorique, La Châtre, 1978, LITP-ENSTA. (In French)

• A Survey of Some Syntactic Results in the Lambda-calculus, with Gérard Berry. Proc. Ann. Conf. on Mathematical Foundations of Computer Science, Olomouc, Tchecoslovaquia, Lecture Notes in Computer Science 74, Springer-Verlag (1979).

• Optimal reductions in the lambda-calculus, To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, edited by J.P.Seldin and J.R.Hindley, Academic Press, 1980. [Pdf].

• Full Abstraction for Sequential Languages: the State of the Art, with Gérard Berry and Pierre-Louis Curien, in Algebraic Methods in Semantics, Cambridge University Press (1985) 89-132. [Pdf].

• Attemps for Generalising the Recursive Path Orderings, with Sam Kamin, Manuscript, 1980. [Pdf].

• "Kruskaleries", Manuscript, October 1981. [Pdf]. (In French)

• "Dershowitzeries", Manuscript, October 1981. [Pdf]. (In French)

• Computations in Orthogonal Rewriting Systems, I, with Gérard Huet, Computational Logic; Essays in Honor of Alan Robinson, edited by J.-L.Lassez and G.Plotkin, The MIT Press, 1991. [Pdf].

• Computations in Orthogonal Rewriting Systems, II, with Gérard Huet, Computational Logic; Essays in Honor of Alan Robinson, edited by J.-L.Lassez and G.Plotkin, The MIT Press, 1991. [Pdf].
  (Also research report 359, INRIA, 1979)

• On the Lucifer System, VLSI architecture, Univ. of Bristol, Edited by B.Randell and P.C.Treleaven. Prentice Hall, 1982. [Pdf].

• L'éditeur Luciole, Unpublished note, with Gérard Baudet, 1983. [Pdf]. (In French)

• Le système Lucifer d'aide à la conception de circuits intégrés, with Jérôme Chailloux, Jean-Marie Hullot and Jean Vuillemin. Rapport de Recherche 196, Mars 1983. [Pdf]. (In French)

• Sharing in the Evaluation of lambda Expressions, in Programming of Future Generation Computers II, edited by K. Fuchi and L.Kott, Elsevier, North Holland, 1988. [Pdf].

• Explicit substitutions, with Martin Abadi, Luca Cardelli and Pierre-Louis Curien. Journal of Functional Programming, Vol. 1(4), pp. 375-416, 1991. [Pdf]. Also presented at the Seventeenth Annual ACM Symposium on Principles of Programming Languages (POPL) 1990. [Pdf].

• A Confluent Calculus of Substitutions, with Thérèse Hardin, France-Japan Artificial Intelligence and Computer Science Symposium, Izu, 1989.

• Confluence properties of Weak and Strong Calculi of Explicit Substitutions, with Thérèse Hardin and Pierre-Louis Curien, Journal of the ACM, 43(2):362--397. 1996. [Pdf].

• The Geometry of Optimal Lambda Reduction, with Martin Abadi and Georges Gonthier Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages (January 1992), pp.15-26. [Pdf].

• Linear Logic Without Boxes, with Martin Abadi and Georges Gonthier, Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (June 1992), pp.223-234. [Pdf].

• An Abstract Standardisation Theorem, with Georges Gonthier and Paul-André Melliès, Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (June 1992), pp.72-81. [Pdf].

• Analysis and Caching of Dependencies, with Martin Abadi and Butler Lampson, Proceedings of the 1996 ACM International Conference on Functional Programming (May 1996), pp.83-91. [Pdf].

• A Calculus of Mobile Agents, with Cédric Fournet, Georges Gonthier, Luc Maranget and Didier Rémy, Proceedings of the 7th International Conference on Concurrency Theory (CONCUR), 1996. [Pdf].

• Some results in the Join-Calculus, Proceedings of the Third International Symposium on the Theoretical Aspects of Computer Software (TACS), Sendai, Japan. Lecture Notes in Computer Science, 1281, Springer-Verlag (1997). [Pdf].

• The weak lambda calculus and Programming Languages, with Luc Maranget, FSTTCS '99: foundations of software technology and theoretical computer science, edited by C.Pandu Rangan, V.Raman, R.Ramanujam. LNCS, 1738, Springer, 1999. [Pdf].

• An asynchronous distributed implementation of Ambients, with Cédric Fournet and Alan Schmitt, Proceedings of the second IFIP Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, edited by J.van Leeuwen, O.Watanabe, M.Hagiya, P.D.Mosses, T.Ito, LNCS, 1872, Springer, pp.348-364, 2000. [Pdf].

• Sharing in the weak lambda-calculus, with Tomasz Blanc and Luc Maranget. Processes, Terms and Cycles: Steps on the Road to Infinity. Essays dedicated to Jan Willem Klop. LNCS 3838, Springer, 2005. [Pdf].

• Sharing in the weak lambda-calculus revisited, with Tomasz Blanc and Luc Maranget. In Reflections on Type Theory, Lambda Calculus, and the Mind, Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday, Erik Barendsen, Herman Geuvers, Venanzio Capretta, Milad Niqui (Eds.) 2007. [Pdf].

• Structures de données. In Encyclopédie de l'informatique et des systèmes d'information. Editor Jean-Eric Pin. Vuibert (Ed.), pp. 919-928, 2008. ISBN : 978-2-7117-4846-4. (In French) [Pdf]

• Generalized Finite developments (2007). In Essays in Honour of Gilles Kahn, Cambridge University Press 2009. ISBN-13: 9780521518253 [Pdf].

• Les Dominos de Wang, Revue Quadrature, "Magazine de mathématiques pures et épicées", 82, Octobre-novembre-décembre 2011 (5 pages). [Pdf]. (In French)

• Redexes are stable in the lambda-calculus. A special issue dedicated to Corrado Böhm for his 90th birthday. Submitted 2012. Published in Mathematical Structures in Computer Science, 27(5), pp. 738-750, 2017. [Pdf].

• The cost of usage in the lambda-calculus, with Andrea Asperti. Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), June 25-28, 2013, New Orleans, USA [Pdf].

• Simple proofs of simple programs in Why3. Essays for the Luca Cardelli Fest, ed. Martin Abadi and Philippa Gardner and Andrew D. Gordon and Radu Mardare, MSR-TR-2014-104, September 2014, Microsoft Research Cambridge [Pdf].

• Readable semi-automatic formal proofs of Depth-First Search on graphs using Why3, with Chen Ran. Submitted, October 2015. [Pdf].

• Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe, with Ran Chen. Journées Francophones des Langages Applicatifs (JFLA), Gourette, January 2017. (In French) [Pdf].

• A Semi-automatic Proof of Strong Connectivity, with Ran Chen. 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), Heidelberg, July 2017. [Pdf].

• Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle, with Ran Chen, Cyril Cohen, Stephan Merz, Laurent Théry. 10th conference on Interactive Theorem Proving (ITP), Portland, USA, September 2019. [Pdf].

• Tracking Redexes in the Lambda Calculus. Submitted at FSP2022. [Pdf].

Volumes

• Algorithmes et programmation, avec Robert Cori. (290 pages) Les Éditions de l'École polytechnique 1992. ISBN 2-7302-0619-1.

• Algorithms, Concurrency and Knowledge, Co-edited with Kanchana Kanchanasut. Proceedings of the First Asian Computing Science Conference (ASIAN), Pathumthani, Thailand, December 11-13, 1995. Lecture Notes in Computer Science 1023, (410 pages), Springer. ISBN: 3540606882.

• Informatique fondamentale (271 pages) Les Éditions de l'École polytechnique 2001. ISBN 2-7302-1004-0.

• Exploring New Frontiers of Theoretical Informatics, Co-edited with Ernst W.Mayr and John C.Mitchell. Proceedings of the IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), 22-27 August 2004, Toulouse, France, (674 pages). Kluwer 2004. ISBN-13: 978-1441954862.

• Introduction à la théorie des langages de programmation, avec Gilles Dowek. (110 pages) Les Éditions de l'École polytechnique 2006. ISBN10 : 2-7302-1333-3.,
  Introduction to the Theory of Programming Languages, (Undergraduate Topics in Computer Science). (108 pages) Springer. ISBN-13: 978-0857290755.

• From Semantics to Computer Science, Essays in Honour of Gilles Kahn. Co-edited with Yves Bertot, Gérard Huet and Gordon Plotkin. (594 pages). Cambridge University Press 2009. ISBN-13: 9780521518253.