[home]

I am a post-doctoral researcher within the "Programming, Logic and Semantics" group PLS at the ITU in Copenhagen, working in the Demtech project run by Carsten Schürmann. My research here is centered on the connections between logic and programming languages, and the application of these connections for developing "trustworthy" software. On a more theoretical level, my work is to investigate the logical nature of computation, as well as the computational nature of logic in general.

Nicolas Guenot, IT University of Copenhagen (office 4C15)


IT Universitetet i København,
Rued Langgaards Vej 7,
2300 København S, Danemark.
e-mail: ngue (at) itu.dk [ or ng (at) demtech.dk ]

If you need or want to sign or to encrypt a message or any file you send to me, my PGP key has id 07A30F19 and is available from the server subkeys.pgp.net, and from this server.

Research Topics


I am a (computational) logician: I work at the interface between mathematical logic and the theory of programming languages. In particular, I am using proof theory with the goal of exploring the computational contents of proofs in various systems, taking ideas from the world of computation to the field of logic. Beyond the scope of pure proof theory, my main interest is in the theory of functional, logic or concurrent programming languages, and the safety of programs in general, when ensured by a logical analysis.

Within the Demtech project, I am working on the logical end of the wide spectrum of fields involved in the formal analysis of implementation techniques involved in electronic voting. Deriving enough trust in these techniques from a theoretical understanding of the pieces of software is quite complicated, and it remains a challenging problem even on the level of pure theory, let alone practice. For a logician, this requires to develop theories and tools, such as proof assistants, that are necessary to mechanically prove complex properties on concurrent programs using cryptographic primitives or other security mechanisms. From a perspective of practical applications of logical theories, the most challenging task among a number of problems is in my opinion the extension of logical foundations of computations to more refined paradigms than the successful functional approach, in particular handling and understanding "concurrency".

Earlier, my PhD thesis was centered on the computational interpretations of proof systems using the deep inference methodology, where inference rules can be applied deep inside a formula. It developped the theory of intuitionistic logic in that setting, its interpretation through variants of the lambda-calculus, and the study of polarisation and of the focusing property in a system for linear logic described in the calculus of structures. I defended my thesis at LIX in April 2013.

More on these topics can be found on my research page.

Teaching


In fall 2014, I was responsible for the "Programming Language Seminar" of the "Software Development and Technology" Master at ITU, teaching session types for processes. Other parts of the course were taught by Daniel Gustafsson, Nicolas Pouillard and Peter Sestoft, covering programming in Haskell and dependent types in Agda, as well as memory models for concurrency.

I also organised a PhD course on structural proof theory, meant as a detailed introduction to this field and presenting its connection, int the Curry-Howard tradition, to the design of well-behaved models of computation.

During fall 2013, I was teaching the "Discrete Mathematics" course with Lorena Ronquillo. In 2011-2012, I was holding an ATER position (temporary research/teaching position) at the university Paris Diderot (Paris 7), where I taught object-oriented programming in Java and imperative programming in C.

Earlier, I was also a teaching assistant at the university of Paris-Nord (Paris 13), located in Villetaneuse, doing exercises/programming sessions for computer science courses. I have also been teaching the basics of programming in C as well as functional programming, in Ocaml and logic programming, in Prolog.

More information on my teaching page.
[research]

I am mostly working on proof theory and on computational aspects of logical systems, with a particular interest for substructural logics and their proof systems, for variants of the lambda-calculus or the pi-calculus and their type systems, proof assistants, as well as for proof search techniques.

Topics


Curry-Howard for concurrency

The extension of the Curry-Howard correspondence from its original grounds in functional programming to the concurrent paradigm has proven to be a challenge, but concurrency has taken much importance over the last one or two decades and it is not yet understood properly from a logical perspective. I am working on the development of a correspondence between processes and proofs in systems for linear logic, following the lines of the original work of Abramsky (and later Bellin and Scott), which has been used in a modified form and extended recently through a connection to session types, explored by Caires and Pfenning as well as Wadler. There is a number of problems with the existing proposals, in particular concerning sequentiality and compositionality, but I believe a more thorough investigation of the logical principles at work will lead to a system just as satisfying as the description of functional programming in something like System F. This is critical if one wants to develop programming languages based on concurrent models of computation.

Reasoning about concurrent programs

Beyond the basic level of designing type systems for concurrent programming languages, the question of the kind of reasoning principles required in order to prove any interesting result about concurrent programs is very much dependent on our logical understanding of concurrency. For example, processes typically come with a notion of equivalence meant to implement their graph-like nature in a linear syntax, and this prevents us from applying the tools previously developped for languages based on well-behaved inductive terms. As a consequence, we need to extend the standard techniques to handle this more complex situation before moving to the next step: the design of proof assistants and provers based on process calculi. Such tools should provide natural ways of reasoning about concurrent programming just as tools like Coq, Agda or Twelf and Abella provide powerful frameworks for reasoning about functional and sequential programs.

A proof-theoretical view of evaluation strategies

In the theory of functional programming languages, the choice of a particular strategy for the evaluation of a program plays a important role: this leads to the distinction between a lazy language such as Haskell and a strict language such as Ocaml. More generally there are many possible strategies to evaluate a given lambda-term, and some of these (such as call-by-name and call-by-value) can be related to particular proof systems for intuitionistic logic. I work on the specific connection between a number of strategies and normal forms of proofs in the sequent calculus, following the methodology of focusing and exploiting the pervasive notion of polarity in logic. The goal of my research is to find a uniform language in which to express various strategies, and providing means to explicitly control reduction through dedicated operators refining the usual language of functional programs.

Nested typing

The novelties introduced into structural proof theory with the deep inference methodology and its syntactic improvements on standard natural deduction or sequent calculi systems can be reflected on computational interpretations of logical systems by the generalisation of standard type systems. In particular, drawing ideas from the formalism of the calculus of structures, and from open deduction, I am investigating a notion of "nested typing" and its application to the design of functional languages involving advanced features, such as communication, explicit sharing or detailed sequentialisation information.

Non-classical logics

The main tool for my research, on the logical side, is linear logic, which is standard logic nowadays, just as much as classical and intuitionistic logics. However, I am interested in various other logical systems, from the usual modal logics and their description by hybrid connectives to variants of linear logic based on non-commutative connectives, induction or coindution using fixpoints, equations on first-order terms, or other extensions. Such logics offer reasoning principles that can be used directly or provide new insights on interesting computational interpretations.

and much more... but I can't do everything at the same time.
[publications]

The documents linked here are made available for the purpose of scientific dissemination, including published articles, but also drafts or technical reports and titles/abstracts/slides of talks, as well as my PhD thesis.

Published papers



Abstracts and Talks


  • Symmetric Normalisation for Intuitionistic Logic
      at CSL/LICS'14 (slides)
  • Session Types, Solos, and the Computational Contents of Sequent Calculus Proofs
      at TYPES'14 (abstract, slides)
  • Linear Session Types for Solos
      at TAFP'13 and MSC'14 (abstract)
  • Nested Typing and Communication in the λ-calculus
      at TYPES'13 (abstract, slides)
  • On the Computational Interpretation of Contraction in Deep Inference
      at PCC'13 (abstract)

PhD thesis


Until 2013, I was a PhD student at LIX (the lab for theoretical computer science at the Ecole Polytechnique), in France, where I was working under the supervision of Lutz Straßburger in the Parsifal team lead by Dale Miller.

My PhD thesis was centered around the methodology of "deep inference" which allows to apply inference rules deep inside a formula. This idea is implemented in the formalism of the calculus of structures, and in nested sequents — formalisms aiming at overcoming important problems generated by the restricted structure of the proofs used in tree-based formalisms such as natural deduction and the sequent calculus.

I defended my thesis on the 10th of April 2013 before:


It is entitled "Nested Deduction in Logical Foundations for Computation", and it aimed at developping the computational interpretation of logical systems using "nested deduction", following the methodology of deep inference. The main contributions are two systems for intuitionistic logic in this nested setting, a generalised normalisation procedure based on permutations of inference rules viewed as rewrite rules, its connection by type systems to lambda-calculi with explicit substitutions, and the definition of an "incrementally focused" normal form in the calculus of structures for linear logic.
[teaching]

Please don't hesitate to send me emails for questions related to teaching. I also have a slot for office hours at ITU between 16:00 and 17:00 on Wednesdays.

Current Teaching


I am not teaching this semester, but I will next fall.

Past Teaching


  • •  IT University of Copenhagen, 2013-...
    •    discrete mathematics (for first year Master students)
    •    advanced programming languages and types (for second year Master students)
    •    structural proof theory (for PhD students)

  • •  Université Paris Diderot (Paris 7), 2012-2013
    •    types and object-oriented programming (first year) in Java
    •    data structures for imperative programming (second year) in C

  • •  Université Paris Nord (Paris 13), 2008-2011
    •    functional programming (third year) in Ocaml
    •    logic programming (third year) in Prolog
    •    imperative programming (first year) in C