research

Writings

Published

[Hyv21]

"Representing Continuous Functions between Greatest Fixed Points of Indexed Containers", Logical Methods in Computer Science, Volume 17, Issue 3, 2021.

We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers can be defined in dependent type theory without any notion of equality but require inductive-recursive definitions. Most of the properties of these constructions only rely on a mild notion of equality (intensional equality) and can thus be formalized in the dependently typed language Agda.

Download: pdf, archive of Agda formalization, online documentation of Agda code

[DHNR17]

"Les démonstrations mathématiques", with René David, Karim Nour and Christophe Raffalli éditions ellipses, 2017. (french)

A book, in French

Ce livre présente le langage utilisé par les mathématiciens en commençant par la construction et la sémantique des énoncés. Les règles de raisonnement à la base de toutes les démonstrations sont ensuite exposées en détail. Nous détaillons également les éléments de français qui permettent d'exprimer les preuves mathématiques par des textes concis, variés et intelligibles.

La seconde moitié de l'ouvrage insiste sur les difficultés de raisonnement et de langage exclusivement à travers d'exemples. La plupart sont tirés du programme du lycée et de première année universitaire; d'autres, ludiques et moins conventionnels, ne nécessitent pas de connaissance supplémentaire.

Les nombreux exercices ne testent pas uniquement les compétences mathématiques mais surtout la compréhension des principes de démonstration. À notre connaissance, ce style d'exercice n'existe dans aucun autre ouvrage. Les corrections proposées ne contiennent pas simplement une démonstration possible mais sont souvent accompagnées de commentaires sur le raisonnement sous-jacent.

Ce livre ne traite pas de logique formelle mais se veut une référence pour un cours de mathématiques sur le raisonnement tel qu'il est pratiqué. L'enseignant y trouvera des exemples et des explications qu'il pourra facilement réutiliser. L'étudiant qui aura assimilé les principes présentés sera mieux armé pour s'attaquer à la compréhension de notions mathématiques plus complexes.

René David, Pierre Hyvernat, Karim Nour et Christophe Raffalli sont des spécialistes de la théorie de la démonstration. Ils sont enseignants chercheurs et membres du laboratoire de mathématiques de l'université Savoie Mont Blanc. Ils sont joignables par email à l'adresse dhnr@univ-smb.fr.

[Hyv14-multi]

"Some Properties of Inclusions of Multisets and Contractive Boolean Functions", 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.

[Hyv14-pf]

"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.

[Hyv14-sct]

"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.

[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 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

[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 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.

[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.

Popular science

Here are some talks I've given to general audience, in French:

Events

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