The Collapse of the Sequential Intersection Type System on the Multiset Intersection Type is Surjective. - Pierre Vial (CoRR, 2016)

Infinitary Intersection Types as Sequences: a New Answer to Klop's Question. - Pierre Vial (CoRR, 2016)

Coinductive Intersection Types are Completely Unsound. - Pierre Vial (CoRR, 2016)

Infinitary intersection types as sequences: A new answer to Klop's problem. - Pierre Vial (LICS, 2017)

Types as Resources for Classical Natural Deduction. - Delia Kesner; Pierre Vial (FSCD, 2017)

Non-idempotent typing operators, beyond the lambda-calculus. (Opérateurs de typage non-idempotents, au delà du lambda-calcul). - Pierre Vial (2017)

Every λ-Term is Meaningful for the Infinitary Relational Model. - Pierre Vial (LICS, 2018)

Polyadic approximations, fibrations and intersection types. - Damiano Mazza; Luc Pellissier; Pierre Vial (Proc. ACM Program. Lang., 2018)

Sequence Types for Hereditary Permutators. - Pierre Vial (FSCD, 2019)

Consuming and Persistent Types for Classical Logic. - Delia Kesner; Pierre Vial (LICS, 2020)

Non-idempotent types for classical calculi in natural deduction style. - Delia Kesner; Pierre Vial (Log. Methods Comput. Sci., 2020)

Sequence Types and Infinitary Semantics. - Pierre Vial (CoRR, 2021)

General Automation in Coq through Modular Transformations. - Valentin Blot; Louise Dubois de Prisque; Chantal Keller; Pierre Vial (PxTP, 2021)

Modular pre-processing for automated reasoning in dependent type theory. - Valentin Blot; Denis Cousineau 002; Enzo Crance; Louise Dubois de Prisque; Chantal Keller; Assia Mahboubi; Pierre Vial (CoRR, 2022)

Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. - Valentin Blot; Denis Cousineau 002; Enzo Crance; Louise Dubois de Prisque; Chantal Keller; Assia Mahboubi; Pierre Vial (CPP, 2023)