[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 ]
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
- Sequent Calculus and Equational Reasoning
with D. Gustafsson, at LFMTP'15 - Computation in Focused Intuitionistic Logic
with T. Brock-Nannestad and D. Gustafsson, at PPDP'15 (pdf) - Focused Linear Logic and the λ-calculus
with T. Brock-Nannestad, at MFPS'15 (pdf) - Hybrid Extensions in a Logical Framework
with T. Brock-Nannestad, A. Murawska and C. Schürmann, at LFMTP'14 (pdf,bib) - Cut Elimination in Multifocused Linear Logic
with T. Brock-Nannestad, at LINEARITY'14 (pdf,bib,CoRR) - Symmetric Normalisation for Intuitionistic Logic
with L. Straßburger, at CSL/LICS'14 (pdf,bib) - Equality and Fixpoints in the Calculus of Structures
with K. Chaudhuri, at CSL/LICS'14 (pdf,bib) - The Focused Calculus of Structures
with K. Chaudhuri and L. Straßburger, at CSL'11 (pdf,bib) - Nested Proof Search as Reduction in the λ-calculus
at PPDP'11 (pdf,bib) - Focused Proof Search for Linear Logic in the Calculus of
Structures
at ICLP'10 (pdf,bib) - Concurrency and Permutability in the Sequent Calculus
at SD'09 (pdf,bib)
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:
- Delia Kesner (reviewer), Université Paris Diderot
- Luca Roversi (reviewer), Università di Torino
- Richard McKinley, Universtät Bern
- Benjamin Werner (chair), INRIA / Ecole Polytechnique
- Dale Miller, INRIA / Ecole Polytechnique
- Lutz Straßburger (supervisor), INRIA / Ecole Polytechnique
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
[links]
Some useful links:
- • to get a bibliography right, DBLP
- • a classic with a serious server name, Stanford's SEP
- • have nice regular meetings with Chocola!
- • open access, yay: LIPIcs
- • also open journal, Logical Methods in Computer Science
- • and open preprints at arXiv
Places where I studied and/or worked:
- • ENS Lyon / LIP
- • Université Paris 7 / PPS
- • Université Paris 13 / LIPN
- • Université Paris 11 / LRI
- • Ecole Polytechnique / LIX
- • Universität Bern / IAM
Random/specific/other:
- • information/protest about the university in France: SLU and SLR
- • a very nice book online, Learn You a Haskell (for great good!)
- • resources for Ocaml
- • also logic programming is nice, here's Teyjus