This page



  1. Logic, linear logic and denotational semantics;
  2. Computer assisted theorem proving;
  3. Automatic termination checker;
  4. Combinatorial game theory.




"Some Properties of Inclusions of Multisets and Contractive Boolean Functions", to appear in Discrete Mathematics, volume 329, 2014.

This short paper follows (and subsumes) the older note [HyvCom04]. It starts from a curious puzzle: call an n-tuple of sets X = (X1, ..., Xn) smaller than Y if it has less "unordered sections". The first section shows that quivalence classes up-to this preorder are very easy to describe (they correspond to changing the order of the n-tuples of sets). The rest of the paper characterizes the preorder in terms of the simpler pointwise inclusion and the existence of specific contractive Boolean functions from B^n to B^n. We also show that contrary to plain Boolean functions or increasing Boolean functions, contractive Boolean functions aren't finitely generated, which might explain why this preorder isn't easily described concretely.

Download: pdf and complete Python script from the appendix. A more complex script that looks for unordered sections that witness that X isn't smaller than Y.


"A Linear Category of Polynomial Functors (extensional part)", Logical Methods in Computer Science, volume 10, issue 2, May 2014.

This is a companion paper to [Hyv13] bellow. It shows how the constructions on representations of polynomial functors can be defined directly on arbitrary functors. (Of course, they aren't always defined outside polynomial ones...)

Download: pdf.


"The Size-Change Termination Principle for Constructor Based Languages", Logical Methods in Computer Science, volume 10, issue 1, February 2014.

This paper describes an automatic termination checker for a generic first-order call-by-value language in ML style. We use the fact that value are built from variants and tuples to keep some information about how arguments of recursive call evolve during evaluation.

The result is a criterion for termination extending the size-change termination principle of Lee, Jones and Ben-Amram that can detect size changes inside subvalues of arguments. Moreover the corresponding algorithm is easy to implement, making it a good candidate for experimentation.

Download: pdf; source code: download or browse online. Standalone mini termination checker for a language with very simple syntax basic-SCT.tar.


"A Linear Category of Polynomial Diagrams", published in Mathematical Structures in Computer Science, volume 24, issue 1, February 2014.

We present a categorical model for intuitionistic linear logic where objects are polynomial diagrams and morphisms are simulation diagrams. The multiplicative structure (tensor product and its adjoint) can be defined in any locally cartesian closed category, whereas the additive (product and coproduct) and exponential Tensor-comonoid comonad) structures require additional properties and are only developed in the category Set, where the objects and morphisms have natural interpretations in terms of games, simulation and strategies.

Download: pdf


"From Coherent to finiteness spaces", Logical Methods in Computer Science, volume 7, issue 3, September 2011.

A short note that presents a new and surprising relation between the categories of coherent spaces and finiteness spaces. The main tool used in this analysis is the infinite Ramsey theorem.

Download: pdf.
"Programming Interfaces and Basic Topology", together with Peter Hancock. Annals of Pure and Applied Logic, volume 137, January 2006.

Download: pdf.

"Synchronous Games, Simulations and lambda-calculus", Games for Logic and Programming Languages, April 2005. Presented in Edinburgh for the "Games for Logic and Programming Languages" Workshop (ETAPS 2005).

Download: pdf.

"Predicate Transformers and Linear Logic: yet another Denotational Model", Lecture Notes in Computer Science, vol. 3210, September 2004. Presented at the CSL 2004 conference.

Download: pdf.

Notes and miscellanea

"A Completeness Theorem for 'Total Boolean Functions'", a short, nice and elementary proof of a completeness theorem for a boolean calculus. This was triggered by discussions with Christine Tasson, who came up with another proof of the same result.

Download: pdf.


"A Logical Investigation of Interaction Systems" , this is my PhD thesis, written part time in Chalmers (Sweden) and part time at the IML (France). My supervisors were Thierry Coquand and Thomas Ehrhard, November 2005.

Download: pdf.


"Predicate Transformers, (co)Monads and Resolutions": some remarks about closures, monads and resolutions, October 2004. (This is how I understood the concept of resolution for a monad: it describes concretely a non trivial resolution for closure/interior operators on powersets...)

Download: pdf; as well as the COQ script mentioned in the paper: script.


"A commutative Product for Sets": a very short note on an unexpected property of the commutative version of the cartesian product, January 2004.

Download: pdf. (Obsolete: see [HyvOrder11] for an extended version.)

"Interaction Systems: a Replacement for Automata?", extended abstract for the Winter Meeting of the computer science department of Chalmers, January 2003.

Download: pdf.

Some slides

Past events

Some things I (co-)organized in the past:

Necessary Reads

Here is a list of things I suggest every mathematician should read, if only for sheer enjoyment...

  1. John Horton Conway, "On Numbers and Games", London Mathematical Society Monographs, 1976. (2nd edition by AK-Peters, 2000).
  2. John Horton Conway, "The Weird and Wonderful Chemistry of Audioactive Decay", Open Problems in Communications and Computation, editors T.M. Cover and B. Gopinath, pp 173--188, Springer 1987.
  3. Andreas Blass, "Seven Trees in One", Journal of Pure and Applied Algebra. vol. 103, pp 1--21, 1995.
  4. John Hortan Conway, "The Sensual (quadratic) Form", especially the first lecture, Carus Mathematical Monographs, 1997.