[my buzzwords]

• linear logic
• classical logic
• intuitionistic logic
• deep inference
• calculus of structures
• logic programming
• functional programming
• lambda-calculus
• explicit substitutions
• resource operators
• term rewriting
• type systems
• efficient reduction
• code sharing
• theorem proving
• proof search
• focusing
• abstract machines
• concurrency
• process algebras
• bureaucracy
• proof-nets
• flashy colours

I'm currently working as a PhD student within the LIX, the theoretical computer science lab of the Ecole Polytechnique and doing research on the connections existing between logic and programming languages, from both a theoretical and a practical viewpoint. I'm part of Parsifal, a (very nice) team lead by Dale Miller, and Lutz Strassburger is my supervisor.

Nicolas Guenot (that's me)

You cannot reach me by phone, because I don't have one here, but you can talk directly to me if you find room 1019 at LIX, where I have my desk, and you can also choose one of the more sophisticated means available, as snail-mail:

Ecole Polytechnique,
Laboratoire d'Informatique (LIX),
rue de Saclay, 91128 Palaiseau cedex, France.

or e-mail: nguenot (concat) lix.polytechnique.fr

If you need or want to sign or crypt a message or some file you send to me, my PGP public key with id 07A30F19 is available from the server subkeys.pgp.net, and (maybe up-to-date) here.

Research

What I'm doing here is mathematical logic, and more precisely proof theory, with the goal of exploring the theory of programming languages from a logical perspective. My main interest is logic and functional programming languages.

My work is mainly based on the deep inference methodology, which allows to apply inference rules deep inside formulas. This idea has been implemented in the calculus of structures, and also in nested sequents, formalisms aiming at overcoming important problems generated by the restricted structure of the sequent calculus.

(yes, I should write more on this... "coming soon", as they say)

Publications:

• [CSL'11] The Focused Calculus of Structures, with Kaustuv Chaudhuri and Lutz Strassburger. (pdf)


• [PPDP'11] Nested Proof Search as Reduction in the λ-calculus. (pdf,bib)


• [ICLP'10] Focused Proof Search for Linear Logic in the Calculus of Structures. (pdf,bib)


• [SD'09] Concurrency and Permutability in the Sequent Calculus. (pdf,bib)

Teaching

I'm also teaching assistant at the university of Paris-Nord (UP13) located in Villetaneuse, doing some exercises and programming sessions for computer science courses.

In 2008-2009 and 2009-2010, I was teaching for the course Elements d'Informatique, organised by Pierre Boudes and Erick Alphonse, which is a general introduction to computer science for first-year students, mainly focused on the use of the C language and imperative programming.

In 2010-2011, I'm teaching for the course of Logic Programming, which is organised by Mario Valencia-Pabon, and the course of Functional Programming, organised by Stefano Guerrini.

Misc.

About politics: there is an important debate going on these days in France (and Europe in general) on the way we should do research, and what kind of education system we want. My opinion is that public research should not be handed over to any private corporation, nor submitted to the same kind of silly mechanisms of performance evaluation, because its goal is not individual profit. Please have a look at the SLR webpage. More importantly education, and in particular universities, is a matter of the highest interest to the society : its goal is to provide everybody with an education, not to create and perpetuate social inequalities. Please have a look at the SLU webpage.

[Last revision : Mon, 06 Jun 2011 15:43 +0200]
Page created with vim, debian gnu/linux, and my little fingers.