Mechanizable Proofs about Parallel Processes - Jean-Marie Cadiou; Jean-Jacques Lévy (SWAT, 1973)

An algebraic interpretation of the lambda beta - calculus and a labeled lambda - calculus. - Jean-Jacques Lévy (Lambda-Calculus and Computer Science Theory, 1975)

An Algebraic Interpretation of the lambda beta K-Calculus; and an Application of a Labelled lambda -Calculus. - Jean-Jacques Lévy (Theor. Comput. Sci., 1976)

A Survey of Some Syntactic Results in the lambda-Calculus. - Gérard Berry; Jean-Jacques Lévy (MFCS, 1979)

Minimal and Optimal Computations of Recursive Programs. - Gérard Berry; Jean-Jacques Lévy (J. ACM, 1979)

Computations in Orthogonal Rewriting Systems, I. - Gérard P. Huet; Jean-Jacques Lévy (Computational Logic - Essays in Honor of Alan Robinson, 1991)

Computations in Orthogonal Rewriting Systems, II. - Gérard P. Huet; Jean-Jacques Lévy (Computational Logic - Essays in Honor of Alan Robinson, 1991)

Explicit Substitutions. - Martín Abadi; Luca Cardelli; Pierre-Louis Curien; Jean-Jacques Lévy (J. Funct. Program., 1991)

Linear Logic Without Boxes - Georges Gonthier; Martín Abadi; Jean-Jacques Lévy (LICS, 1992)

An abstract standardisation theorem - Georges Gonthier; Jean-Jacques Lévy; Paul-André Melliès (LICS, 1992)

The Geometry of Optimal Lambda Reduction. - Georges Gonthier; Martín Abadi; Jean-Jacques Lévy (POPL, 1992)

A Calculus of Mobile Agents. - Cédric Fournet; Georges Gonthier; Jean-Jacques Lévy; Luc Maranget; Didier Rémy (CONCUR, 1996)

Analysis and Caching of Dependencies. - Martín Abadi; Butler W. Lampson; Jean-Jacques Lévy (ICFP, 1996)

Confluence Properties of Weak and Strong Calculi of Explicit Substitutions. - Pierre-Louis Curien; Thérèse Hardin; Jean-Jacques Lévy (J. ACM, 1996)

Some Results in the Joint-Calculus. - Jean-Jacques Lévy (TACS, 1997)

Explicit Substitutions and Programming Languages. - Jean-Jacques Lévy; Luc Maranget (FSTTCS, 1999)

An Asynchronous, Distributed Implementation of Mobile Ambients. - Cédric Fournet; Jean-Jacques Lévy; Alan Schmitt (IFIP TCS, 2000)

Introduction - Bohm's theorem: applications to Computer Science Theory - BOTH 2001. - Jean-Jacques Lévy (BOTH, 2001)

Sharing in the Weak Lambda-Calculus. - Tomasz Blanc; Jean-Jacques Lévy; Luc Maranget (Processes, Terms and Cycles, 2005)

Introduction to the Theory of Programming Languages. - Gilles Dowek; Jean-Jacques Lévy (Springer, 2011)

The Cost of Usage in the Lambda-Calculus. - Andrea Asperti; Jean-Jacques Lévy (LICS, 2013)

A Semi-automatic Proof of Strong Connectivity. - Ran Chen; Jean-Jacques Lévy (VSTTE, 2017)

Redexes are stable in the λ-calculus. - Jean-Jacques Lévy (Math. Struct. Comput. Sci., 2017)

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. - Ran Chen; Cyril Cohen; Jean-Jacques Lévy; Stephan Merz; Laurent Théry (CoRR, 2018)

Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. - Ran Chen; Cyril Cohen; Jean-Jacques Lévy; Stephan Merz; Laurent Théry (ITP, 2019)

Tracking Redexes in the Lambda Calculus. - Jean-Jacques Lévy (The French School of Programming, 2024)