The Psyche prover

The Ψ project

Dr Stéphane Graham-Lengrand

Chargé de Recherche au CNRS
Professeur Chargé de Cours à l'École Polytechnique

 2006/2007: Royal Scottish Academy.

I graduated from the Royal Scottish Academy of Music and Drama with a Postgraduate Diploma in Cello Performing.

I received tuition from Robert Irvine, who also coached our quartet. "The Cosmopolitan Quartet" won the Governor's prize for Chamber Music and the Mabel Glover Prize for String quartet, both at the RSAMD, and performed in various placed such as the Reid Concert Hall in Edinburgh. Along with other students of the RSAMD, I also joined the Scottish Ensemble's December tour.

 2003/2006: St Andrews & Paris.

I completed my Philosophy Doctorate at the School of Computer Science, University of St Andrews, Scotland and at PPS Laboratory, University Paris VII, France.

I was supervised by Dr Roy DYCKHOFF and Pr. Delia KESNER

My thesis, entitled Normalisation & Equivalence in Proof Theory & Type Theory, was publicly defended on Friday 8th December 2006 before

Dr Pierre-Louis CURIEN, Chairman
Dr James McKINNA, Internal examiner of St Andrews
Pr. Gilles DOWEK, Referee (rapporteur) for Paris VII
Pr. Luke ONG, Referee (rapporteur) for St Andrews
Pr. Henk BARENDREGT, Examiner
Pr. Dale MILLER, Examiner
& my supervisors.

For this thesis I was one of the three recipients of the 2007 Ackermann Award, the EACSL Outstanding Dissertation Award for Logic in Computer Science, presented at the conference CSL'2007 in Lausanne.

More information


 2002/2003: Paris.

As a third year scholar of the ENS, I completed a Master of Science, which we call in France DEA (Diplôme d'Etudes Approfondies), at the PPS laboratory in Paris:

DEA Programmation : Sémantique, Preuves et Langages

- Linear Logic (R. Di Cosmo & D. Kesner)
- Game Semantics (P.-A. Mellies & O. Laurent)
- Concurrency & Biology (V. Danos & V. Schachter)
- Type, Category & Domain theory (G. Longo & A. Bucciarelli)
- Subtyping & Object languages (G. Castagna)
- Process Calculi (P.-L. Curien)
- Typing & Programming (F. Pottier)
- Type Theory (B. Werner)
- Lambda-calculus (T. Hardin)
- Rewriting (D. Kesner & J.-P. Jouannaud)

I also did the research at the PPS Laboratory with Professor Delia Kesner. It is about resource control operators in lambda-calculus with explicit substitutions. Here is the postscript file (770 Ko).


At the same time, I also graduated from the Sorbonne with a Bachelor of Arts in English (Language, Literature and Civilization):

Major in History of English (especially Old English).


Case studies in Literature:
- W. Shakespeare, King Lear
- L. Sterne, Tristram Shandy
- S. Fitzgerald, Tender Is the Night
- E. Dickinson, selected poems.


 2001/2002: University of Oxford.

As a second year scholar of the ENS, I had the opportunity to study at Oxford University, as a member of University College.

I completed a Master of Science in Mathematics and the Foundations of Computer Science at the Mathematical Institute, where I took the following modules, which reflect more or less my scientific interests :


Axiomatic Set Theory (Prof. Wilkie, my supervisor)
Model Theory (Prof. Zilber)
Gödel Incompleteness Thorems (Dr. Isaacson)
Domain Theory (Prof. Roscoe)
Communication Theory (Prof. Welsh and Prof. Mc Diarmid)
Game Semantics (Prof. Abramsky)
Computational Algebra (Prof. Vaughan-Lee)

I also did the research part at the Computing Laboratory, where I wrote a dissertation under the supervision of Professor Samson Abramsky. It is about Curry-Howard correspondence for classical sequent calculus, cut-elimination and explicit substitutions. Here is the postscript file (700 Ko).


 2000/2001: Ecole Normale Supérieure in Lyon.

As part of my first year curriculum in the ENS in Lyon, I have done a research project in Lambda-Calculus under the supervision of Professor Pierre Lescanne, who ushered me in the attractive world of theoretical computer science and computational logic.

The project consisted in characterizing strongly normalizing terms, in a lambda-calculus with explicit substitutions, by a typing system with intersections. That is, finding a way of assigning types to terms such that the typable terms are precisely the terms the computation of which always terminates.

The dissertation : (.ps)

The complete proof : (.ps)


 1998/2000: Lycée Hoche, Versailles.

I studied in the "classes préparatoires" in the Lycée Hoche: MPSI for the first year, then MP* for the second year (mostly Maths, Physics, and Computer Science).

The examination determining the admission as a scholar of the ENS of Lyon required the students to present a short personal work. I had chosen to develop and implement a computational method to extract from an input signal its "musical meaning", using a wavelet transform. The score that it yields is rather rough, although not worthless.

The report: (winzip compressed .doc)