Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

20 résultats
Page :
triés par
Image document

Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types

 Valentin Blot , Jim Laird
33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Jul 2018, Oxford, United Kingdom. pp.95-104, ⟨10.1145/3209108.3209206⟩
Communication dans un congrès hal-01766887v1
Image document

Realizability for Peano arithmetic with winning conditions in HON games

 Valentin Blot
Annals of Pure and Applied Logic, 2017, 168 (2), pp.254 - 277. ⟨10.1016/j.apal.2016.10.006⟩
Article dans une revue hal-01766884v1
Image document

Vers une traduction de K en Dedukti

 Amélie Ledein , Valentin Blot , Catherine Dubois
JFLA 2022 - Journées Francophones des Langages Applicatifs (JFLA), Jun 2022, Saint-Médard-d'Excideuil, France
Communication dans un congrès hal-03604962v1
Image document

Classical Extraction in Continuation Models

 Valentin Blot
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Jun 2016, Porto, Portugal. pp.13:1-13:17, ⟨10.4230/LIPIcs.FSCD.2016.13⟩
Communication dans un congrès hal-01766872v1
Image document

Realizability for Peano Arithmetic with Winning Conditions in HON Games

 Valentin Blot
Typed Lambda Calculi and Applications, Jun 2013, Eindhoven, Netherlands. pp.77 - 92, ⟨10.1007/978-3-642-38946-7_8⟩
Communication dans un congrès hal-00793324v4
Image document

Quasi-Affine Transformation in Higher Dimension

 Valentin Blot , David Coeurjolly
Discrete Geometry for Computer Imagery, Sep 2009, Montréal, Canada. pp.493 - 504, ⟨10.1007/978-3-642-04397-0_42⟩
Communication dans un congrès hal-01092499v1
Image document

Quasi-Affine Transformation in 3-D: Theory and Algorithms

 David Coeurjolly , Valentin Blot , Marie-Andrée Jacob-da Col
Combinatorial Image Analysis, Nov 2009, Playa del Carmen, Mexico. pp.68 - 81, ⟨10.1007/978-3-642-10210-3_6⟩
Communication dans un congrès hal-01092500v1
Image document

An interpretation of system F through bar recursion

 Valentin Blot
32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Jun 2017, Reykjavik, Iceland. ⟨10.1109/LICS.2017.8005066⟩
Communication dans un congrès hal-01766883v1
Image document

SMTCoq: automatisation expressive et extensible dans Coq

 Valentin Blot , Amina Bousalem , Quentin Garchery , Chantal Keller
JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
Communication dans un congrès hal-02369249v1
Image document

Diller-Nahm Bar Recursion

 Valentin Blot
FSCD 2023 - 8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy. pp.32:1-32:16, ⟨10.4230/LIPIcs.FSCD.2023.32⟩
Communication dans un congrès hal-04144888v1
Image document

On Bar Recursion and Choice in a Classical Setting

 Valentin Blot , Colin Riba
Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Dec 2013, Melbourne, Australia. pp.349-364, ⟨10.1007/978-3-319-03542-0_25⟩
Communication dans un congrès hal-00835540v1
Image document

An Implementation of Set Theory with Pointed Graphs in Dedukti

 Valentin Blot , Gilles Dowek , Thomas Traversié
LFMTP 2022 - International Workshop on Logical Frameworks and Meta-Languages : Theory and Practice, Aug 2022, Haïfa, Israel
Communication dans un congrès hal-03740004v1
Image document

From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory

 Valentin Blot , Gilles Dowek , Thomas Traversié , Théo Winterhalter
FoSSaCS 2024 - 27th International Conference on Foundations of Software Science and Computation Structures, Apr 2024, Luxembourg City, Luxembourg. pp.3-23, ⟨10.1007/978-3-031-57231-9_1⟩
Communication dans un congrès hal-04275229v2
Image document

General Automation in Coq through Modular Transformations

 Valentin Blot , Louise Dubois de Prisque , Chantal Keller , Pierre Vial
Seventh Workshop on Proof Exchange in Theorem Proving, Jul 2021, Pittsburgh, United States. ⟨10.4204/EPTCS.336.3⟩
Communication dans un congrès hal-03328935v1
Image document

Bécassine à la chasse au Coq (démonstration)

 Valentin Blot , Louise Dubois de Prisque , Chantal Keller , Pierre Vial
JFLA 2022 - Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France
Communication dans un congrès hal-03604902v1
Image document

A direct computational interpretation of second-order arithmetic via update recursion

 Valentin Blot
LICS 2022 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haïfa, Israel. ⟨10.1145/3531130.3532458⟩
Communication dans un congrès hal-03698879v1
Image document

Compositional pre-processing for automated reasoning in dependent type theory

 Valentin Blot , Denis Cousineau , Enzo Crance , Louise Dubois de Prisque , Chantal Keller , et al.
CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
Communication dans un congrès hal-03901019v3
Image document

Typed realizability for first-order classical analysis

 Valentin Blot
Logical Methods in Computer Science, 2015, 11 (4), pp.1 - 43. ⟨10.2168/LMCS-11(4:22)2015⟩
Article dans une revue hal-01766871v1
Image document

Hybrid realizability for intuitionistic and classical choice

 Valentin Blot
31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, Jul 2016, New York, United States. ⟨10.1145/2933575.2934511⟩
Communication dans un congrès hal-01766881v1
Image document

A semantics of K into dedukti

 Amélie Ledein , Valentin Blot , Catherine Dubois
TYPES 2022 - 28th International Conference on Types for Proofs and Programs (TYPES), Jul 2023, Nantes, France. ⟨10.4230/LIPIcs.TYPES.2022.23⟩
Communication dans un congrès hal-03895834v2
Page :