Filtrer vos résultats
- 20
- 18
- 2
- 20
- 1
- 4
- 3
- 1
- 1
- 1
- 2
- 2
- 1
- 2
- 2
- 17
- 3
- 10
- 9
- 4
- 4
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 20
- 4
- 3
- 3
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
20 résultats
|
|
triés par
|
|
Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types33rd 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
|
||
|
An interpretation of system F through bar recursion32nd 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
|
||
|
SMTCoq: automatisation expressive et extensible dans CoqJFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
Communication dans un congrès
hal-02369249v1
|
||
|
Realizability for Peano arithmetic with winning conditions in HON gamesAnnals of Pure and Applied Logic, 2017, 168 (2), pp.254 - 277. ⟨10.1016/j.apal.2016.10.006⟩
Article dans une revue
hal-01766884v1
|
||
|
Vers une traduction de K en DeduktiJFLA 2022 - Journées Francophones des Langages Applicatifs (JFLA), Jun 2022, Saint-Médard-d'Excideuil, France
Communication dans un congrès
hal-03604962v1
|
||
|
On Bar Recursion and Choice in a Classical SettingProgramming 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
|
||
|
An Implementation of Set Theory with Pointed Graphs in DeduktiLFMTP 2022 - International Workshop on Logical Frameworks and Meta-Languages : Theory and Practice, Aug 2022, Haïfa, Israel
Communication dans un congrès
hal-03740004v1
|
||
|
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo TheoryFoSSaCS 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
|
||
|
Classical Extraction in Continuation Models1st 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
|
||
|
Realizability for Peano Arithmetic with Winning Conditions in HON GamesTyped 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
|
||
|
Quasi-Affine Transformation in Higher DimensionDiscrete 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
|
||
|
Diller-Nahm Bar RecursionFSCD 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
|
||
|
Quasi-Affine Transformation in 3-D: Theory and AlgorithmsCombinatorial 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
|
||
|
General Automation in Coq through Modular TransformationsSeventh Workshop on Proof Exchange in Theorem Proving, Jul 2021, Pittsburgh, United States. ⟨10.4204/EPTCS.336.3⟩
Communication dans un congrès
hal-03328935v1
|
||
|
Bécassine à la chasse au Coq (démonstration)JFLA 2022 - Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France
Communication dans un congrès
hal-03604902v1
|
||
|
A direct computational interpretation of second-order arithmetic via update recursionLICS 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
|
||
|
Typed realizability for first-order classical analysisLogical Methods in Computer Science, 2015, 11 (4), pp.1 - 43. ⟨10.2168/LMCS-11(4:22)2015⟩
Article dans une revue
hal-01766871v1
|
||
|
Hybrid realizability for intuitionistic and classical choice31st 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
|
||
|
A semantics of K into deduktiTYPES 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
|
||
|
Compositional pre-processing for automated reasoning in dependent type theoryCPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
Communication dans un congrès
hal-03901019v3
|