Pierre Vial

According to our database, Pierre Vial authored at least 15 papers between 2016 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of five.

2023

Compositional Pre-processing for Automated Reasoning in Dependent Type Theory.

Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022

Modular pre-processing for automated reasoning in dependent type theory.

Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial

CoRR, 2022

2021

General Automation in Coq through Modular Transformations.

Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial

Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

Sequence Types and Infinitary Semantics.

Pierre Vial

CoRR, 2021

2020

Non-idempotent types for classical calculi in natural deduction style.

Delia Kesner, Pierre Vial

Log. Methods Comput. Sci., 2020

Consuming and Persistent Types for Classical Logic.

Delia Kesner, Pierre Vial

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

2019

Sequence Types for Hereditary Permutators.

Pierre Vial

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018

Polyadic approximations, fibrations and intersection types.

Damiano Mazza, Luc Pellissier, Pierre Vial

Proc. ACM Program. Lang., 2018

Every λ-Term is Meaningful for the Infinitary Relational Model.

Pierre Vial

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

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

Pierre Vial

PhD thesis, 2017

Types as Resources for Classical Natural Deduction.

Delia Kesner, Pierre Vial

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Infinitary intersection types as sequences: A new answer to Klop's problem.

Pierre Vial

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

2016

Coinductive Intersection Types are Completely Unsound.

Pierre Vial

CoRR, 2016

Infinitary Intersection Types as Sequences: a New Answer to Klop's Question.

Pierre Vial

CoRR, 2016

The Collapse of the Sequential Intersection Type System on the Multiset Intersection Type is Surjective.

Pierre Vial

CoRR, 2016