"Research"
Interests
 Logic, linear logic and denotational semantics;
 Computer assisted theorem proving;
 Automatic termination checker;
 Combinatorial game theory.
Writings
Published
 [Hyv14multi]
 "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 ntuple of sets X = (X1, ..., Xn) smaller than Y if it has less "unordered sections". The first section shows that quivalence classes upto this preorder are very easy to describe (they correspond to changing the order of the ntuples 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.
 [Hyv14pf]
 "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.
 [Hyv14sct]
 "The SizeChange 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 firstorder callbyvalue 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 sizechange termination principle of Lee, Jones and BenAmram 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 basicSCT.tar.
 [Hyv13]
 "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 Tensorcomonoid 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
 [Hyv11]
 "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.
 [HaHy06]
 "Programming Interfaces and Basic Topology", together with Peter Hancock. Annals of Pure and Applied Logic, volume 137, January 2006. Download: pdf.
 [Hyv05]
 "Synchronous Games, Simulations and lambdacalculus", Games for Logic and Programming Languages, April 2005. Presented in Edinburgh for the "Games for Logic and Programming Languages" Workshop (ETAPS 2005). Download: pdf.
 [Hyv04]
 "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
 [Hyv08]
 "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.
 [HyvPhD]
 "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.
 [HyvResol04]
 "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.
 [HyvCom04]

"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.)  [HyvAut03]
 "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
 exposé « amphis pour tous » sur l'origami : supports « mathématiques et origami » (novembre 2013, en français, exposé grand public)
 exposé « amphis pour tous » sur les jeux : La science des jeux (décembre 2009, en français, exposé grand public)
Past events
Some things I (co)organized in the past:
 organizer of the Réalisabilité à Chambéry (#6) workshop (June 2013)
 organizer of the Réalisabilité à Chambéry (#5) workshop (June 2012)
 organizer of the Réalisabilité à Chambéry (#4) workshop (June 2011)
 organizer of the Réalisabilité à Chambéry (#3) workshop (June 2010)
 coorganizer of the École jeunes chercheurs du GDR IM (Mars 2010)
 organizer of the second Réalisabilité à Chambéry workshop (June 2009)
 coorganizer of the TYPES meeting (May 2009)
 organizer of the Réalisabilité à Chambéry (June 2008)
 program committee for the GaLoP III workshop, part of the ETAPS 2008 in Budapest, Hungary: Games for Logic and Programming (April 2008)
 organizing and program committee for the LAC meeting in Chambéry: Douzième réunion du groupe de travail Logique, Algèbre et Calcul (February 2007)
Necessary Reads
Here is a list of things I suggest every mathematician should read, if only for sheer enjoyment...
 John Horton Conway, "On Numbers and Games", London Mathematical Society Monographs, 1976. (2nd edition by AKPeters, 2000).
 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 173188, Springer 1987.
 Andreas Blass, "Seven Trees in One", Journal of Pure and Applied Algebra. vol. 103, pp 121, 1995.
 John Hortan Conway, "The Sensual (quadratic) Form", especially the first lecture, Carus Mathematical Monographs, 1997.